:: The Differentiable Functions on Normed Linear Spaces
:: by Hiroshi Imura , Morishige Kimura and Yasunari Shidama
::
:: Received May 24, 2004
:: Copyright (c) 2004-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, REAL_1, NORMSP_1, SEQ_1, NAT_1, PRE_TOPC,
RCOMP_1, TARSKI, CARD_1, ARYTM_3, ARYTM_1, XXREAL_0, RELAT_1, FUNCT_1,
SEQ_2, ORDINAL2, STRUCT_0, VALUED_0, SUPINF_2, RLVECT_1, VALUED_1,
COMPLEX1, XXREAL_2, FDIFF_1, ZFMISC_1, PARTFUN1, FUNCOP_1, FUNCT_2,
LOPBAN_1, XBOOLE_0, FCONT_1, RSSPACE, NFCONT_1, CFCONT_1, LOPBAN_2;
notations TARSKI, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, PRE_TOPC,
XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, ORDINAL1, NUMBERS, REAL_1, NAT_1,
RLVECT_1, STRUCT_0, FUNCOP_1, VALUED_0, VALUED_1, SEQ_1, SEQ_2, VFUNCT_1,
NORMSP_0, NORMSP_1, RSSPACE, LOPBAN_1, LOPBAN_2, NFCONT_1, FDIFF_1,
RECDEF_1;
constructors REAL_1, SQUARE_1, COMPLEX1, SEQ_2, FDIFF_1, RSSPACE, VFUNCT_1,
LOPBAN_3, NFCONT_1, RECDEF_1, RELSET_1, BINOP_2, RVSUM_1, COMSEQ_2,
NUMBERS;
registrations FUNCT_1, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, MEMBERED,
FDIFF_1, STRUCT_0, LOPBAN_1, LOPBAN_2, VALUED_0, VALUED_1, FUNCT_2,
FUNCOP_1, NAT_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions TARSKI, XBOOLE_0, NFCONT_1, NORMSP_1, STRUCT_0;
equalities XBOOLE_0, RLVECT_1, SUBSET_1, VALUED_1, STRUCT_0;
expansions TARSKI, XBOOLE_0, NFCONT_1, NORMSP_1, STRUCT_0;
theorems TARSKI, ABSVALUE, XBOOLE_0, XBOOLE_1, SUBSET_1, RELSET_1, RLVECT_1,
XCMPLX_0, XCMPLX_1, ZFMISC_1, FUNCOP_1, SEQ_1, SEQ_2, NAT_1, SEQM_3,
RELAT_1, FUNCT_1, VFUNCT_1, FUNCT_2, SEQ_4, NORMSP_1, LOPBAN_1, LOPBAN_2,
LOPBAN_3, PARTFUN1, PARTFUN2, NFCONT_1, XREAL_1, COMPLEX1, XXREAL_0,
ORDINAL1, VALUED_1, STRUCT_0, VALUED_0, VECTSP_1, NORMSP_0, NUMBERS;
schemes NAT_1, SEQ_1, RECDEF_1, FUNCT_2;
begin :: Differentiable Function on Normed Linear Spaces
reserve n,k for Element of NAT;
reserve x,y,X for set;
reserve g,r,p for Real;
reserve S for RealNormSpace;
reserve rseq for Real_Sequence;
reserve seq,seq1 for sequence of S;
reserve x0 for Point of S;
reserve Y for Subset of S;
:: Normed Linear Spaces varsions of RCOMP_1:37 -
:: RCOMP_1:37 --> NFCONT_1:4
theorem Th1:
for x0 be Point of S for N1,N2 being Neighbourhood of x0 ex N
being Neighbourhood of x0 st N c= N1 & N c= N2
proof
let x0 be Point of S;
let N1,N2 be Neighbourhood of x0;
consider g1 be Real such that
A1: 0<g1 and
A2: {y where y is Point of S: ||.y-x0 .|| < g1} c= N1 by NFCONT_1:def 1;
consider g2 be Real such that
A3: 0<g2 and
A4: {y where y is Point of S: ||.y-x0 .|| < g2} c= N2 by NFCONT_1:def 1;
set g = min(g1,g2);
take {y where y is Point of S: ||.y-x0 .|| < g};
A5: g<=g2 by XXREAL_0:17;
A6: {y where y is Point of S: ||.y-x0 .|| < g} c= {y where y is Point of S:
||.y-x0 .|| < g2}
proof
let z be object;
assume z in {y where y is Point of S: ||.y-x0 .|| < g};
then consider y be Point of S such that
A7: z=y and
A8: ||.y-x0 .|| < g;
||.y-x0 .|| < g2 by A5,A8,XXREAL_0:2;
hence thesis by A7;
end;
A9: g<=g1 by XXREAL_0:17;
A10: {y where y is Point of S: ||.y-x0 .|| < g} c= {y where y is Point of S:
||.y-x0 .|| < g1}
proof
let z be object;
assume z in {y where y is Point of S: ||.y-x0 .|| < g};
then consider y be Point of S such that
A11: z=y and
A12: ||.y-x0 .|| < g;
||.y-x0 .|| < g1 by A9,A12,XXREAL_0:2;
hence thesis by A11;
end;
0<g by A1,A3,XXREAL_0:15;
hence thesis by A2,A4,A10,A6,NFCONT_1:3;
end;
theorem Th2:
for X being Subset of S st X is open for r be Point of S st r in
X ex N being Neighbourhood of r st N c= X
proof
let X be Subset of S;
assume X is open;
then
A1: X` is closed;
let r be Point of S;
assume that
A2: r in X and
A3: for N be Neighbourhood of r holds not N c= X;
defpred P[Element of NAT,Point of S] means $2 in {y where y is Point of S:
||.y-r.|| < 1/($1+1)} & $2 in X`;
A4: now
let g be Real such that
A5: 0<g;
set N={y where y is Point of S:||.y-r.|| < g};
N is Neighbourhood of r by A5,NFCONT_1:3;
then not N c= X by A3;
then consider x be object such that
A6: x in N and
A7: not x in X;
consider s be Point of S such that
A8: x=s and
A9: ||.s-r.|| <g by A6;
take s;
thus s in N by A9;
thus s in X` by A7,A8,XBOOLE_0:def 5;
end;
A10: for n ex s be Point of S st P[n,s]
proof
let n;
0 < 1 * (n + 1)";
then 0 < 1/(n + 1) by XCMPLX_0:def 9;
hence thesis by A4;
end;
consider s1 be sequence of S such that
A11: for n being Element of NAT holds P[n,s1.n] from FUNCT_2:sch 3(A10);
A12: rng s1 c= X`
proof
let x be object;
assume x in rng s1;
then consider y be object such that
A13: y in dom s1 and
A14: s1.y=x by FUNCT_1:def 3;
reconsider y as Element of NAT by A13;
s1.y in X` by A11;
hence thesis by A14;
end;
A15: now
let p be Real;
assume
A16: 0<p;
consider n being Nat such that
A17: p"<n by SEQ_4:3;
p" + 0 < n + 1 by A17,XREAL_1:8;
then 1/(n+1) < 1/p" by A16,XREAL_1:76;
then
A18: 1/(n+1) < p by XCMPLX_1:216;
take n;
let m be Nat;
A19: m in NAT by ORDINAL1:def 12;
assume n<=m;
then
A20: n + 1 <= m + 1 by XREAL_1:6;
s1.m in {y where y is Point of S:||.y-r.|| < 1/(m+1)} by A11,A19;
then
A21: ex y be Point of S st s1.m=y & ||.y-r.|| < 1/(m+1);
1/(m+1) <= 1/(n+1) by A20,XREAL_1:118;
then ||.s1.m - r.|| < 1/(n+1) by A21,XXREAL_0:2;
hence ||.s1.m - r.|| <p by A18,XXREAL_0:2;
end;
then
A22: s1 is convergent;
then lim s1 = r by A15,NORMSP_1:def 7;
then r in X` by A22,A12,A1;
hence contradiction by A2,XBOOLE_0:def 5;
end;
theorem
for X being Subset of S st X is open for r be Point of S st r in X
holds ex g st 0<g & {y where y is Point of S:||.y-r.|| < g} c= X
proof
let X be Subset of S such that
A1: X is open;
let r be Point of S;
assume r in X;
then consider N be Neighbourhood of r such that
A2: N c= X by A1,Th2;
consider g such that
A3: 0<g & {y where y is Point of S:||.y-r.|| < g} c= N by NFCONT_1:def 1;
take g;
thus thesis by A2,A3;
end;
theorem Th4:
for X being Subset of S holds ((for r be Point of S st r in X
holds ex N be Neighbourhood of r st N c= X) implies X is open )
proof
let X be Subset of S;
assume that
A1: for r be Point of S st r in X holds ex N be Neighbourhood of r st N
c= X and
A2: not X is open;
not X` is closed by A2;
then consider s1 be sequence of S such that
A3: rng s1 c= X` and
A4: s1 is convergent and
A5: not lim s1 in X`;
consider N be Neighbourhood of (lim s1) such that
A6: N c= X by A1,A5,SUBSET_1:29;
consider g be Real such that
A7: 0<g and
A8: {y where y is Point of S:||.y-(lim s1).|| < g} c= N by NFCONT_1:def 1;
consider n being Nat such that
A9: for m be Nat st n<=m holds ||.(s1.m) - (lim s1).||<g by A4,A7,
NORMSP_1:def 7;
n in NAT by ORDINAL1:def 12;
then n in dom s1 by FUNCT_2:def 1;
then
A10: s1.n in rng s1 by FUNCT_1:def 3;
||.s1.n - (lim s1).|| <g by A9;
then s1.n in {y where y is Point of S:||.y-(lim s1).|| < g};
then s1.n in N by A8;
hence contradiction by A3,A6,A10,XBOOLE_0:def 5;
end;
theorem
for X being Subset of S holds ( (for r be Point of S st r in X holds
ex N be Neighbourhood of r st N c= X) iff X is open) by Th2,Th4;
:: Normed Linear Spaces versions of SEQ_1: -
definition
let X be set, S be ZeroStr;
let f be Function of X,S;
redefine attr f is non-zero means :: redefines non-zero (STRUCT_0, definition)
rng f c= NonZero S;
compatibility
proof
thus
f is non-zero implies rng f c= NonZero S
by ZFMISC_1:34;
assume
A1: rng f c= NonZero S;
assume 0.S in rng f;
then not 0.S in {0.S} by A1,XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end;
end;
theorem Th6:
seq is non-zero iff for x st x in NAT holds seq.x<>0.S
proof
thus seq is non-zero implies for x st x in NAT holds seq.x<>0.S
proof
assume seq is non-zero;
then
A1: rng seq c= NonZero S;
let x;
assume x in NAT;
then x in dom seq by FUNCT_2:def 1;
then seq.x in rng seq by FUNCT_1:def 3;
then not seq.x in {0.S} by A1,XBOOLE_0:def 5;
hence thesis by TARSKI:def 1;
end;
assume
A2: for x st x in NAT holds seq.x<>0.S;
now
let y be object;
assume
A3: y in rng seq;
then ex x being object st x in dom seq & seq.x=y by FUNCT_1:def 3;
then y<>0.S by A2;
then not y in {0.S} by TARSKI:def 1;
hence y in NonZero S by A3,XBOOLE_0:def 5;
end;
then rng seq c= NonZero S;
hence thesis;
end;
theorem Th7:
seq is non-zero iff for n being Nat holds seq.n<>0.S
proof
thus seq is non-zero implies for n being Nat holds seq.n<>0.S
by ORDINAL1:def 12,Th6;
assume for n being Nat holds seq.n<>0.S;
then for x holds x in NAT implies seq.x<>0.S;
hence thesis by Th6;
end;
definition
let RNS be RealLinearSpace;
let S be sequence of RNS;
let a be Real_Sequence;
func a (#) S -> sequence of RNS means
:Def2:
for n being Nat holds it.n = a.n * S.n;
existence
proof
deffunc F(Element of NAT) = a.$1 * S.$1;
consider S being sequence of RNS such that
A1: for n holds S.n = F(n) from FUNCT_2:sch 4;
take S;
let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A1;
end;
uniqueness
proof
let S1, S2 be sequence of RNS;
assume that
A2: for n being Nat holds S1.n = a.n * S.n and
A3: for n being Nat holds S2.n = a.n * S.n;
for n holds S1.n = S2.n
proof
let n;
S1.n = a.n * S.n by A2;
hence thesis by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;
definition
let RNS be RealLinearSpace;
let z be Point of RNS;
let a be Real_Sequence;
func a * z -> sequence of RNS means
:Def3:
for n being Nat holds it.n = a.n * z;
existence
proof
deffunc F(Element of NAT) = a.$1 * z;
consider S being sequence of RNS such that
A1: for n holds S.n = F(n) from FUNCT_2:sch 4;
take S;
let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A1;
end;
uniqueness
proof
let S1, S2 be sequence of RNS;
assume that
A2: for n being Nat holds S1.n = a.n * z and
A3: for n being Nat holds S2.n = a.n * z;
for n holds S1.n = S2.n
proof
let n;
S1.n = a.n * z by A2;
hence thesis by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem
for rseq1,rseq2 be Real_Sequence holds (rseq1+rseq2)(#)seq=rseq1(#)seq
+rseq2(#)seq
proof
let rseq1,rseq2 be Real_Sequence;
now
let n;
thus ((rseq1+rseq2)(#)seq).n =(rseq1+rseq2).n*seq.n by Def2
.=(rseq1.n+rseq2.n)*seq.n by SEQ_1:7
.=rseq1.n*seq.n+rseq2.n*seq.n by RLVECT_1:def 6
.=(rseq1(#)seq).n+rseq2.n*seq.n by Def2
.=(rseq1(#)seq).n+(rseq2(#)seq).n by Def2
.=((rseq1(#)seq)+(rseq2(#)seq)).n by NORMSP_1:def 2;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th9:
for rseq be Real_Sequence for seq1, seq2 be sequence of S holds
rseq(#)(seq1+seq2)=rseq(#)seq1+rseq(#)seq2
proof
let rseq be Real_Sequence;
let seq1, seq2 be sequence of S;
now
let n;
thus (rseq(#)(seq1+seq2)).n =rseq.n*(seq1+seq2).n by Def2
.=rseq.n*(seq1.n+seq2.n ) by NORMSP_1:def 2
.=rseq.n*seq1.n+rseq.n*seq2.n by RLVECT_1:def 5
.=(rseq(#)seq1).n+rseq.n*seq2.n by Def2
.=(rseq(#)seq1).n+(rseq(#)seq2).n by Def2
.=((rseq(#)seq1)+(rseq(#)seq2)).n by NORMSP_1:def 2;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th10:
for rseq be Real_Sequence holds r*(rseq(#)seq) =rseq(#)(r*seq)
proof
let rseq be Real_Sequence;
now
let n;
thus (r*(rseq(#)seq)).n =r*(rseq(#)seq).n by NORMSP_1:def 5
.=r*(rseq.n*seq.n) by Def2
.=(r*rseq.n)*seq.n by RLVECT_1:def 7
.=rseq.n*(r*seq.n) by RLVECT_1:def 7
.=rseq.n*(r*seq).n by NORMSP_1:def 5
.=(rseq(#)(r*seq)).n by Def2;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for rseq1,rseq2 be Real_Sequence holds (rseq1-rseq2)(#)seq=rseq1(#)seq
-rseq2(#)seq
proof
let rseq1,rseq2 be Real_Sequence;
now
let n;
thus ((rseq1-rseq2)(#)seq).n =(rseq1+-rseq2).n*seq.n by Def2
.=(rseq1.n+(-rseq2).n)*seq.n by SEQ_1:7
.=(rseq1.n+-rseq2.n)*seq.n by SEQ_1:10
.=(rseq1.n-rseq2.n)*seq.n
.=rseq1.n*seq.n-rseq2.n*seq.n by RLVECT_1:35
.=(rseq1(#)seq).n-rseq2.n*seq.n by Def2
.=(rseq1(#)seq).n-(rseq2(#)seq).n by Def2
.=((rseq1(#)seq)-(rseq2(#)seq)).n by NORMSP_1:def 3;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th12:
for rseq be Real_Sequence for seq1, seq2 be sequence of S holds
rseq(#)(seq1-seq2)=rseq(#)seq1-rseq(#)seq2
proof
let rseq be Real_Sequence;
let seq1, seq2 be sequence of S;
now
let n;
thus (rseq(#)(seq1-seq2)).n =rseq.n*(seq1-seq2).n by Def2
.=rseq.n*(seq1.n-seq2.n ) by NORMSP_1:def 3
.=rseq.n*seq1.n-rseq.n*seq2.n by RLVECT_1:34
.=(rseq(#)seq1).n-rseq.n*seq2.n by Def2
.=(rseq(#)seq1).n-(rseq(#)seq2).n by Def2
.=((rseq(#)seq1)-(rseq(#)seq2)).n by NORMSP_1:def 3;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th13:
rseq is convergent & seq is convergent implies rseq (#) seq is convergent
proof
assume that
A1: rseq is convergent and
A2: seq is convergent;
consider g1 be Real such that
A3: for p be Real st 0<p ex n be Nat st for m be
Nat st n<=m holds |.rseq.m-g1.|<p by A1,SEQ_2:def 6;
consider g2 be Point of S such that
A4: for p be Real st 0<p
ex n be Nat st for m be Nat st n<=m holds ||.seq.m-g2.||<p
by A2;
reconsider g1 as Real;
take g=g1*g2;
let p;
rseq is bounded by A1,SEQ_2:13;
then consider r be Real such that
A5: 0<r and
A6: for n be Nat holds |.rseq.n.|<r by SEQ_2:3;
reconsider r as Real;
A7: 0+0<||.g2.||+r by A5,NORMSP_1:4,XREAL_1:8;
assume
A8: 0<p;
then consider n1 be Nat such that
A9: for m be Nat st n1<=m holds |.rseq.m-g1.|<p/(||.g2.||+r
) by A3,A7,XREAL_1:139;
consider n2 be Nat such that
A10: for m be Nat st n2<=m holds ||.seq.m-g2.||<p/(||.g2.||+r
) by A4,A7,A8,XREAL_1:139;
reconsider n=n1+n2 as Nat;
take n;
let m be Nat such that
A11: n<=m;
n1<=n1+n2 by NAT_1:12;
then n1<=m by A11,XXREAL_0:2;
then
A12: |.rseq.m-g1.|<=p/(||.g2.||+r) by A9;
0<=||.g2.|| & ||.(rseq.m-g1)*g2.||=||.g2.||*|.rseq.m-g1.| by NORMSP_1:4
,def 1;
then
A13: ||.(rseq.m-g1)*g2.||<=||.g2.||*(p/(||.g2.||+r)) by A12,XREAL_1:64;
||.((rseq(#)seq).m)-g.|| =||.rseq.m*seq.m-g1*g2.|| by Def2
.=||.rseq.m*seq.m-0.S-g1*g2.|| by RLVECT_1:13
.=||.rseq.m*seq.m-(rseq.m*g2-rseq.m*g2)-g1*g2.|| by RLVECT_1:15
.=||.(rseq.m*seq.m-rseq.m*g2+rseq.m*g2)-g1*g2.|| by RLVECT_1:29
.=||.rseq.m*(seq.m-g2)+rseq.m*g2-g1*g2.|| by RLVECT_1:34
.=||.rseq.m*(seq.m-g2)+(rseq.m*g2-g1*g2).|| by RLVECT_1:def 3
.=||.rseq.m*(seq.m-g2)+(rseq.m-g1)*g2.|| by RLVECT_1:35;
then
A14: ||.((rseq(#)seq).m)-g.||<= ||.rseq.m*(seq.m-g2).||+||.(rseq.m-g1)*g2.||
by NORMSP_1:def 1;
n2<=n by NAT_1:12;
then n2<=m by A11,XXREAL_0:2;
then
A15: ||.seq.m-g2.||<p/(||.g2.||+r) by A10;
A16: 0<=|.rseq.m.| & 0<=||.seq.m-g2.|| by COMPLEX1:46,NORMSP_1:4;
|.rseq.m.|<r by A6;
then |.rseq.m.|*||.seq.m-g2.||<r*(p/(||.g2.||+r)) by A16,A15,XREAL_1:96;
then
A17: ||.rseq.m*(seq.m-g2).||<r*(p/(||.g2.||+r)) by NORMSP_1:def 1;
r*(p/(||.g2.||+r))+||.g2.||*(p/(||.g2.||+r)) =(p/(||.g2.||+r))*(||.g2 .||+r)
.=p by A7,XCMPLX_1:87;
then ||.rseq.m*(seq.m-g2).||+||.(rseq.m-g1)*g2.||<p by A17,A13,XREAL_1:8;
hence thesis by A14,XXREAL_0:2;
end;
theorem Th14:
rseq is convergent & seq is convergent implies lim (rseq (#) seq
) = (lim rseq) * (lim seq)
proof
assume that
A1: rseq is convergent and
A2: seq is convergent;
set g2= lim seq;
reconsider g1 = lim rseq as Real;
set g=g1*g2;
rseq is bounded by A1,SEQ_2:13;
then consider r be Real such that
A3: 0<r and
A4: for n be Nat holds |.rseq.n.|<r by SEQ_2:3;
reconsider r as Real;
A5: 0+0<||.g2.||+r by A3,NORMSP_1:4,XREAL_1:8;
A6: 0<=||.g2.|| by NORMSP_1:4;
A7: for p be Real st 0<p
ex n be Nat st for m be Nat
st n <=m holds ||.((rseq(#)seq).m)-g.||<p
proof
let p be Real;
assume 0<p;
then
A8: 0<p/(||.g2.||+r) by A5,XREAL_1:139;
then consider n1 be Nat such that
A9: for m be Nat st n1<=m holds |.rseq.m-g1.|<p/(||.g2.||
+r) by A1,SEQ_2:def 7;
consider n2 be Nat such that
A10: for m be Nat st n2<=m holds ||.seq.m-g2.||<p/(||.g2.||
+r) by A2,A8,NORMSP_1:def 7;
take n=n1+n2;
let m be Nat such that
A11: n<=m;
n1<=n1+n2 by NAT_1:12;
then n1<=m by A11,XXREAL_0:2;
then
A12: |.rseq.m-g1.|<=p/(||.g2.||+r) by A9;
||.(rseq.m-g1)*g2.||=||.g2.||*|.rseq.m-g1.| by NORMSP_1:def 1;
then
A13: ||.(rseq.m-g1)*g2.||<=||.g2.||*(p/(||.g2.||+r)) by A6,A12,XREAL_1:64;
A14: 0<=|.rseq.m.| & 0<=||.seq.m-g2.|| by COMPLEX1:46,NORMSP_1:4;
n2<=n by NAT_1:12;
then n2<=m by A11,XXREAL_0:2;
then
A15: ||.seq.m-g2.||<p/(||.g2.||+r) by A10;
||.((rseq(#)seq).m)-g.|| =||.rseq.m*seq.m-g1*g2.|| by Def2
.=||.rseq.m*seq.m-0.S-g1*g2.|| by RLVECT_1:13
.=||.rseq.m*seq.m-(rseq.m*g2-rseq.m*g2)-g1*g2.|| by RLVECT_1:15
.=||.(rseq.m*seq.m-rseq.m*g2+rseq.m*g2)-g1*g2.|| by RLVECT_1:29
.=||.rseq.m*(seq.m-g2)+rseq.m*g2-g1*g2.|| by RLVECT_1:34
.=||.rseq.m*(seq.m-g2)+(rseq.m*g2-g1*g2).|| by RLVECT_1:def 3
.=||.rseq.m*(seq.m-g2)+(rseq.m-g1)*g2.|| by RLVECT_1:35;
then
A16: ||.((rseq(#)seq).m)-g.||<= ||.rseq.m*(seq.m-g2).||+||.(rseq.m-g1)*g2
.|| by NORMSP_1:def 1;
|.rseq.m.|<r by A4;
then |.rseq.m.|*||.seq.m-g2.||<r*(p/(||.g2.||+r)) by A14,A15,XREAL_1:96;
then
A17: ||.rseq.m*(seq.m-g2).||<r*(p/(||.g2.||+r)) by NORMSP_1:def 1;
r*(p/(||.g2.||+r))+||.g2.||*(p/(||.g2.||+r)) =(p/(||.g2.||+r))*(||.g2
.||+r)
.=p by A5,XCMPLX_1:87;
then ||.rseq.m*(seq.m-g2).||+||.(rseq.m-g1)*g2.||<p by A17,A13,XREAL_1:8;
hence thesis by A16,XXREAL_0:2;
end;
(rseq (#) seq) is convergent by A1,A2,Th13;
hence thesis by A7,NORMSP_1:def 7;
end;
theorem Th15:
for k being Nat
holds (seq+seq1) ^\k=(seq ^\k) +(seq1 ^\k)
proof let k be Nat;
now
let n;
thus ((seq+seq1) ^\k).n=(seq+seq1).(n+k) by NAT_1:def 3
.=seq.(n+k) + seq1.(n+k) by NORMSP_1:def 2
.=(seq ^\k).n +seq1.(n+k) by NAT_1:def 3
.=(seq ^\k).n +(seq1 ^\k).n by NAT_1:def 3
.=((seq ^\k) +(seq1 ^\k)).n by NORMSP_1:def 2;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th16:
(seq-seq1) ^\k=(seq ^\k) -(seq1 ^\k)
proof
now
let n;
thus ((seq-seq1) ^\k).n=(seq-seq1).(n+k) by NAT_1:def 3
.=seq.(n+k) - seq1.(n+k) by NORMSP_1:def 3
.=(seq ^\k).n -seq1.(n+k) by NAT_1:def 3
.=(seq ^\k).n -(seq1 ^\k).n by NAT_1:def 3
.=((seq ^\k) -(seq1 ^\k)).n by NORMSP_1:def 3;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th17:
seq is non-zero implies seq ^\k is non-zero
proof
assume
A1: seq is non-zero;
now
let n be Nat;
(seq ^\k).n=seq.(n+k) by NAT_1:def 3;
hence (seq ^\k).n<>0.S by A1,Th7;
end;
hence thesis by Th7;
end;
definition
let S;
let x be Point of S;
let IT be sequence of S;
attr IT is x-convergent means
:Def4:
IT is convergent & lim IT = x;
end;
theorem Th18:
for X be RealNormSpace for seq be sequence of X holds seq is
constant implies ( seq is convergent & for k be Element of NAT holds lim seq =
seq.k )
proof
let X be RealNormSpace;
let seq be sequence of X;
assume
A1: seq is constant;
then consider r be Point of X such that
A2: for n be Nat holds seq.n=r by VALUED_0:def 18;
thus
A3: seq is convergent by A1,LOPBAN_3:12;
now
let k be Element of NAT;
now
let p be Real such that
A4: 0<p;
reconsider n=0 as Nat;
take n;
let m be Nat such that
n<=m;
||.(seq.m)-(seq.k).||=||.r-(seq.k).|| by A2
.=||.r-r.|| by A2
.=||.0.X.|| by RLVECT_1:15
.=0 by NORMSP_1:1;
hence ||.(seq.m)-(seq.k).||<p by A4;
end;
hence lim seq = seq.k by A3,NORMSP_1:def 7;
end;
hence thesis;
end;
theorem Th19:
for r be Real st 0<r & (for n being Nat holds seq.n=(1/(n+r))*x0) holds
seq is convergent
proof
let r be Real;
assume that
A1: 0<r and
A2: for n being Nat holds seq.n=(1/(n+r))*x0;
take g = 0.S;
let p be Real;
assume
A3: 0<p;
ex pp be Real st pp > 0 & pp*||.x0.|| < p
proof
take pp=p/(||.x0.||+1);
A4: ||.x0.||+0 < ||.x0.||+1 & 0 <= ||.x0.|| by NORMSP_1:4,XREAL_1:8;
A5: ||.x0.||+1 > 0+0 by NORMSP_1:4,XREAL_1:8;
then 0 < p/( ||.x0.||+1 ) by A3,XREAL_1:139;
then pp* ||.x0.|| < pp*(||.x0.|| + 1) by A4,XREAL_1:97;
hence thesis by A3,A5,XCMPLX_1:87;
end;
then consider pp be Real such that
A6: pp > 0 and
A7: pp*||.x0.|| < p;
consider k1 be Nat such that
A8: pp"<k1 by SEQ_4:3;
pp"+0<k1+r by A1,A8,XREAL_1:8;
then 1/(k1+r)<1/pp" by A6,XREAL_1:76;
then
A9: 1/(k1+r)<1*pp"" by XCMPLX_0:def 9;
reconsider k1 as Element of NAT by ORDINAL1:def 12;
take n=k1;
let m be Nat;
assume n<=m;
then
A10: n+r<=m+r by XREAL_1:6;
A11: 0 <= ||.x0.|| by NORMSP_1:4;
1/(m+r)<=1/(n+r) by A1,A10,XREAL_1:118;
then 1/(m+r)<pp by A9,XXREAL_0:2;
then
A12: (1/(m+r))*||.x0.|| <= pp* ||.x0.|| by A11,XREAL_1:64;
||.seq.m-g.|| = ||.(1/(m+r))*x0 - 0.S.|| by A2
.= ||.(1/(m+r))*x0.|| by RLVECT_1:13
.= |.1/(m+r).|*||.x0.|| by NORMSP_1:def 1
.= (1/(m+r))*||.x0.|| by A1,ABSVALUE:def 1;
hence thesis by A7,A12,XXREAL_0:2;
end;
theorem Th20:
for r be Real st 0<r &
(for n being Nat holds seq.n=(1/(n+r))*x0 ) holds lim seq=0.S
proof
let r be Real;
assume that
A1: 0<r and
A2: for n being Nat holds seq.n=1/(n+r)*x0;
A3: now
let p;
A4: 0 <= ||.x0.|| by NORMSP_1:4;
assume
A5: 0<p;
ex pp be Real st pp > 0 & pp*||.x0.|| < p
proof
take pp=p/(||.x0.||+1);
A6: ||.x0.||+0 < ||.x0.||+1 & 0 <= ||.x0.|| by NORMSP_1:4,XREAL_1:8;
A7: ||.x0.||+1 > 0+0 by NORMSP_1:4,XREAL_1:8;
then 0 < p/(||.x0.||+1) by A5,XREAL_1:139;
then pp* ||.x0.|| < pp*(||.x0.|| + 1) by A6,XREAL_1:97;
hence thesis by A5,A7,XCMPLX_1:87;
end;
then consider pp be Real such that
A8: pp > 0 and
A9: pp*||.x0.|| < p;
consider k1 be Nat such that
A10: pp"<k1 by SEQ_4:3;
pp"+0<k1+r by A1,A10,XREAL_1:8;
then 1/(k1+r)<1/pp" by A8,XREAL_1:76;
then
A11: 1/(k1+r)<1*pp"" by XCMPLX_0:def 9;
reconsider n=k1 as Nat;
take n;
let m be Nat;
assume n<=m;
then
A12: n+r<=m+r by XREAL_1:6;
1/(m+r)<=1/(n+r) by A1,A12,XREAL_1:118;
then 1/(m+r)<pp by A11,XXREAL_0:2;
then
A13: (1/(m+r))*||.x0.|| <= pp* ||.x0.|| by A4,XREAL_1:64;
||.seq.m-0.S.|| = ||.(1/(m+r))*x0 - 0.S.|| by A2
.= ||.(1/(m+r))*x0.|| by RLVECT_1:13
.= |.1/(m+r).|*||.x0.|| by NORMSP_1:def 1
.= (1/(m+r))*||.x0.|| by A1,ABSVALUE:def 1;
hence ||.seq.m-0.S.||<p by A9,A13,XXREAL_0:2;
end;
seq is convergent by A1,A2,Th19;
hence thesis by A3,NORMSP_1:def 7;
end;
registration
let S be non trivial RealNormSpace;
cluster non-zero (0.S)-convergent for sequence of S;
existence
proof
consider x0 be Point of S such that
A1: x0 <> 0.S by STRUCT_0:def 18;
deffunc F(Nat) = (1/($1+1))*x0;
consider s1 be sequence of S such that
A2: for n holds s1.n=F(n) from FUNCT_2:sch 4;
A3: for n being Nat holds s1.n=F(n)
proof let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A2;
end;
take s1;
now
let n be Nat;
(n+1)" <> 0;
then
A4: 1/(n+1) <> 0 by XCMPLX_1:215;
thus s1.n <> 0.S
proof
assume s1.n = 0.S;
then (1/(n+1))*x0 = 0.S by A3;
hence contradiction by A1,A4,RLVECT_1:11;
end;
end;
hence s1 is non-zero by Th7;
A5: lim s1 = 0.S by A3,Th20;
s1 is convergent by A3,Th19; then
s1 is (0.S)-convergent by A5;
hence thesis;
end;
end;
registration
let S be RealNormSpace;
cluster (0.S)-convergent for sequence of S;
existence
proof
set x0 = the Point of S ;
deffunc F(Nat) = (1/($1+1))*x0;
consider s1 be sequence of S such that
A1: for n holds s1.n=F(n) from FUNCT_2:sch 4;
A2: for n being Nat holds s1.n=F(n)
proof let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A1;
end;
take s1;
A3: lim s1 = 0.S by A2,Th20;
s1 is convergent by A2,Th19; then
s1 is (0.S)-convergent by A3;
hence thesis;
end;
end;
theorem
for a be 0-convergent non-zero Real_Sequence
for z be Point of S st z <> 0.S
holds a*z is non-zero (0.S)-convergent
proof
let a be 0-convergent non-zero Real_Sequence;
let z be Point of S such that
A1: z <> 0.S;
now
let n be Nat;
A2: a.n <> 0 by SEQ_1:5;
assume (a*z).n = 0.S;
then a.n*z = 0.S by Def3;
hence contradiction by A1,A2,RLVECT_1:11;
end;
hence a*z is non-zero by Th7;
A3: now
let p;
assume
A4: 0<p;
ex pp be Real st pp > 0 & pp*||.z.|| < p
proof
take pp=p/(||.z.||+1);
A5: ||.z.||+0 < ||.z.||+1 & 0 <= ||.z.|| by NORMSP_1:4,XREAL_1:8;
A6: ||.z.||+1 > 0+0 by NORMSP_1:4,XREAL_1:8;
then 0 < p/(||.z.||+1) by A4,XREAL_1:139;
then pp* ||.z.|| < pp*(||.z.|| + 1) by A5,XREAL_1:97;
hence thesis by A4,A6,XCMPLX_1:87;
end;
then consider pp be Real such that
A7: pp > 0 and
A8: pp*||.z.|| < p;
a is convergent & lim a =0;
then consider n be Nat such that
A9: for m be Nat st n <= m holds |.a.m- 0 .| < pp by A7,SEQ_2:def 7;
reconsider n as Nat;
take n;
let m be Nat;
assume n<=m;
then
A10: |.a.m-0 .| < pp by A9;
A11: ||.(a*z).m-0.S.|| = ||.a.m*z - 0.S.|| by Def3
.= ||.a.m*z.|| by RLVECT_1:13
.= |.a.m.|*||.z.|| by NORMSP_1:def 1;
0 <= ||.z.|| by NORMSP_1:4;
then |.a.m.|*||.z.|| <= pp* ||.z.|| by A10,XREAL_1:64;
hence ||.(a*z).m-0.S.||<p by A8,A11,XXREAL_0:2;
end;
hence a*z is convergent;
hence thesis by A3,NORMSP_1:def 7;
end;
theorem
(for r be Point of S holds r in Y iff r in the carrier of S) iff Y=the
carrier of S
proof
thus (for r be Point of S holds r in Y iff r in the carrier of S) implies Y=
the carrier of S
proof
assume for r be Point of S holds r in Y iff r in the carrier of S;
then for y being object holds y in Y iff y in the carrier of S;
hence thesis by TARSKI:2;
end;
assume
A1: Y=the carrier of S;
let r be Point of S;
thus r in Y implies r in the carrier of S;
thus thesis by A1;
end;
reserve S,T for RealNormSpace;
reserve f,f1,f2 for PartFunc of S,T;
reserve s1 for sequence of S;
reserve x0 for Point of S;
registration
let S;
cluster constant for sequence of S;
existence
proof
reconsider s1 = NAT --> 0.S as sequence of S;
take s1;
thus thesis;
end;
end;
:: Normed Linear Spaces versions of FDIFF_1
reserve h for (0.S)-convergent sequence of S;
reserve c for constant sequence of S;
definition
let S,T;
let IT be PartFunc of S,T;
attr IT is RestFunc-like means
:Def5:
IT is total & for h st h is non-zero holds (||.h.||")(#)(IT
/*h) is convergent & lim ((||.h.||")(#)(IT/*h)) = 0.T;
end;
registration
let S,T;
cluster RestFunc-like for PartFunc of S,T;
existence
proof
reconsider f = (the carrier of S) --> 0.T as PartFunc of S,T;
take f;
thus f is total;
A1: dom f = the carrier of S;
now
let h ;
assume h is non-zero ;
now
let n be Nat;
A2: f/.(h.n) =f.(h.n) by A1,PARTFUN1:def 6
.=0.T;
A3: rng h c= dom f;
A4: n in NAT by ORDINAL1:def 12;
thus ((||.h.||")(#)(f/*h)).n = (||.h.||").n*((f/*h).n) by Def2
.= (||.h.||").n*(f/.(h.n)) by A3,A4,FUNCT_2:109
.= 0.T by A2,RLVECT_1:10;
end;
then (||.h.||")(#)(f/*h) is constant & ((||.h.||")(#)(f/*h)).0 = 0.T by
VALUED_0:def 18;
hence
(||.h.||")(#)(f/*h) is convergent & lim ((||.h.||")(#)(f/*h)) = 0.T
by Th18;
end;
hence thesis;
end;
end;
definition
let S,T;
mode RestFunc of S,T is RestFunc-like PartFunc of S,T;
end;
theorem
for R be PartFunc of S,T st R is total holds
R is RestFunc-like iff
for r be Real st r > 0 ex d be Real st d > 0 &
for z be Point of S st z <> 0.S &
||.z.|| < d holds ( ||.z.||"* ||. R/.z .||) < r
proof
let R be PartFunc of S,T such that
A1: R is total;
A2: now
assume
A3: R is RestFunc-like;
assume not
(for r be Real st r > 0
ex d be Real st d > 0 & for z be Point
of S st z <> 0.S & ||.z.|| < d holds ( ||.z.||"* ||. R/.z .||) < r );
then consider r be Real such that
A4: r > 0 and
A5: for d be Real st d > 0
ex z be Point of S st z <> 0.S & ||.z
.|| < d & not ( ||.z.||"* ||. R/.z .||) < r;
defpred P[Nat,Point of S] means $2 <> 0.S & ||.$2.|| < (1/($1+1
)) & not ( ( ||.$2.||"* ||. R/.$2 .||) < r );
A6: for n be Element of NAT ex z be Point of S st P[n,z]
proof
let n be Element of NAT;
0 < 1 * (n + 1)";
then 0 < 1/(n + 1) by XCMPLX_0:def 9;
hence thesis by A5;
end;
consider s be sequence of S such that
A7: for n being Element of NAT holds P[n,s.n] from FUNCT_2:sch 3(A6);
A8: for n being Nat holds P[n,s.n]
proof let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A7;
end;
A9: now
let p be Real;
assume
A10: 0<p;
consider n being Nat such that
A11: p"<n by SEQ_4:3;
p" + 0 < n + 1 by A11,XREAL_1:8;
then 1/(n+1) < 1/p" by A10,XREAL_1:76;
then
A12: 1/(n+1) < p by XCMPLX_1:216;
reconsider n as Nat;
take n;
let m be Nat;
assume n<=m;
then
A13: n + 1 <= m + 1 by XREAL_1:6;
||.s.m.|| < (1/(m+1)) by A8;
then
A14: ||.s.m-0.S.|| < (1/(m+1)) by RLVECT_1:13;
1/(m+1) <= 1/(n+1) by A13,XREAL_1:118;
then ||.s.m - 0.S.|| < 1/(n+1) by A14,XXREAL_0:2;
hence ||.s.m - 0.S.|| <p by A12,XXREAL_0:2;
end;
then
A15: s is convergent;
then
lim s = 0.S by A9,NORMSP_1:def 7;
then reconsider s as (0.S)-convergent sequence of S
by A15,Def4;
s is non-zero by A8,Th7;
then
(||.s.||")(#)(R/*s) is convergent & lim ((||.s.||")(#)(R/*s)) = 0.T
by A3;
then consider n be Nat such that
A16: for m be Nat st n <=m holds ||. ((||.s.||")(#)(R/*s)).
m- 0.T.|| < r by A4,NORMSP_1:def 7;
A17: n in NAT by ORDINAL1:def 12;
A18: ||. ((||.s.||")(#)(R/*s)).n- 0.T.|| < r by A16;
s.n <> 0.S by A8;
then ||.s.n.|| <> 0 by NORMSP_0:def 5;
then
A19: ||.s.n.|| > 0 by NORMSP_1:4;
A20: ||.(||.s.n.||)"*(R/.(s.n)).|| = |.(||.s.n.||)".| * ||.(R/.(s.n)).||
by NORMSP_1:def 1
.=(||.s.n.||)" * ||.(R/.(s.n)).|| by A19,ABSVALUE:def 1;
dom R = the carrier of S by A1,PARTFUN1:def 2;
then
A21: rng s c= dom R;
||. ((||.s.||")(#)(R/*s)).n- 0.T.|| = ||. ((||.s.||")(#)(R/*s)).n .||
by RLVECT_1:13
.= ||.(||.s.||".n)*((R/*s).n).|| by Def2
.= ||.(||.s.||.n)"*((R/*s).n).|| by VALUED_1:10
.= ||.(||.s.n.||)"*((R/*s).n).|| by NORMSP_0:def 4
.= ||.(||.s.n.||)"*(R/.(s.n)).|| by A21,FUNCT_2:109,A17;
hence
for r be Real
st r > 0 ex d be Real st d > 0 & for z be Point of S st
z <> 0.S & ||.z.|| < d holds ( ||.z.||"* ||. R/.z .||) < r
by A8,A18,A20;
end;
now
assume
A22: for r be Real st r > 0
ex d be Real st d > 0 & for z be Point of
S st z <> 0.S & ||.z.|| < d holds ( ||.z.||"* ||. R/.z .||) < r;
now
let s be (0.S)-convergent sequence of S
such that A23: s is non-zero;
A24: s is convergent & lim s = 0.S by Def4;
A25: now
let r be Real;
assume r > 0;
then consider d be Real such that
A26: d > 0 and
A27: for z be Point of S st z <> 0.S & ||.z.|| < d holds ( ||.z.||
"* ||. R/.z .||) < r by A22;
consider n be Nat such that
A28: for m be Nat st n <=m holds ||.s.m-0.S.|| < d by A24,A26,
NORMSP_1:def 7;
take n;
thus for m be Nat st n <=m holds ||. ((||.s.||")(#)(R/*s)).
m- 0.T.|| < r
proof
dom R = the carrier of S by A1,PARTFUN1:def 2;
then
A29: rng s c= dom R;
let m be Nat;
A30: m in NAT by ORDINAL1:def 12;
assume n <=m;
then ||.s.m-0.S .|| < d by A28;
then
A31: ||.s.m.|| < d by RLVECT_1:13;
A32: s.m <> 0.S by Th7,A23;
then ||.s.m.|| <> 0 by NORMSP_0:def 5;
then ||.s.m.|| > 0 by NORMSP_1:4;
then
(||.s.m.||)" * ||.(R/.(s.m)).|| =|.(||.s.m.||)".| * ||.(R/.(s.
m)).|| by ABSVALUE:def 1
.= ||.(||.s.m.||)"*(R/.(s.m)).|| by NORMSP_1:def 1
.= ||.(||.s.m.||)"*((R/*s).m).|| by A29,FUNCT_2:109,A30
.= ||.(||.s.||.m)"*((R/*s).m).|| by NORMSP_0:def 4
.= ||.(||.s.||".m)*((R/*s).m).|| by VALUED_1:10
.= ||. ((||.s.||")(#)(R/*s)).m .|| by Def2
.= ||. ((||.s.||")(#)(R/*s)).m- 0.T.|| by RLVECT_1:13;
hence thesis by A27,A31,A32;
end;
end;
hence (||.s.||")(#)(R/*s) is convergent;
hence lim ((||.s.||")(#)(R/*s)) = 0.T by A25,NORMSP_1:def 7;
end;
hence R is RestFunc-like by A1;
end;
hence thesis by A2;
end;
theorem Th24:
for R be RestFunc of S,T for s be (0.S)-convergent sequence of S
st s is non-zero
holds (R/*s) is convergent & lim (R/*s) = 0.T
proof
let R be RestFunc of S,T;
let s be (0.S)-convergent sequence of S
such that A1: s is non-zero ;
A2: (||.s.||") (#) (R/*s) is convergent by Def5,A1;
now
let n be Element of NAT;
s.n <> 0.S by Th7,A1;
then
A3: ||.s.n.|| <> 0 by NORMSP_0:def 5;
thus (||.s.||(#) ( (||.s.||") (#) (R/*s) )).n =||.s.||.n*((||.s.||")(#)(R
/*s)).n by Def2
.=||.s.||.n*((||.s.||").n*((R/*s).n)) by Def2
.= ||.s.n.||*((||.s.||").n*((R/*s).n)) by NORMSP_0:def 4
.= ||.s.n.||*((||.s.||.n)"*((R/*s).n)) by VALUED_1:10
.= ||.s.n.||*((||.s.n.||)"*((R/*s).n)) by NORMSP_0:def 4
.= ||.s.n.||*(||.s.n.||)"*((R/*s).n) by RLVECT_1:def 7
.= 1*(R/*s).n by A3,XCMPLX_0:def 7
.=(R/*s).n by RLVECT_1:def 8;
end;
then
A4: ||.s.||(#) ( (||.s.||") (#) (R/*s) )= (R/*s) by FUNCT_2:63;
A5: s is convergent by Def4;
then
A6: ||.s.|| is convergent by LOPBAN_1:41;
lim s = 0.S by Def4;
then lim ( ||.s.|| ) = ||.0.S.|| by A5,LOPBAN_1:41;
then
A7: lim ( ||.s.|| ) =0 by NORMSP_1:1;
lim ((||.s.||") (#) (R/*s) ) = 0.T by Def5,A1;
then lim (R/*s) = 0* 0.T by A5,A4,A2,A7,Th14,LOPBAN_1:41;
hence thesis by A4,A2,A6,Th13,RLVECT_1:10;
end;
reserve R,R1,R2 for RestFunc of S,T;
reserve L,L1,L2 for Point of R_NormSpace_of_BoundedLinearOperators(S,T);
theorem Th25:
for h1,h2 be PartFunc of S,T for seq be sequence of S holds h1
is total & h2 is total implies (h1+h2)/*seq = h1/*seq + h2/*seq & (h1-h2)/*seq
= h1/*seq - h2/*seq
proof
let h1,h2 be PartFunc of S,T;
let seq be sequence of S;
assume h1 is total & h2 is total;
then h1+h2 is total by VFUNCT_1:32;
then dom (h1+h2) = the carrier of S by PARTFUN1:def 2;
then dom h1 /\ dom h2 = the carrier of S by VFUNCT_1:def 1;
then
A1: rng seq c= dom h1 /\ dom h2;
hence (h1+h2)/*seq = h1/*seq + h2/*seq by NFCONT_1:12;
thus thesis by A1,NFCONT_1:12;
end;
theorem Th26:
for h be PartFunc of S,T for seq be sequence of S for r be Real
holds h is total implies (r(#)h)/*seq = r*(h/*seq)
proof
let h be PartFunc of S,T;
let seq be sequence of S;
let r be Real;
assume h is total;
then dom h = the carrier of S by PARTFUN1:def 2;
then rng seq c= dom h;
hence thesis by NFCONT_1:13;
end;
theorem Th27:
f is_continuous_in x0 iff x0 in dom f & for s1 be sequence of S
st rng s1 c= dom f & s1 is convergent & lim s1=x0 &
(for n being Nat holds s1.n<>x0)
holds f/*s1 is convergent & f/.x0=lim(f/*s1)
proof
thus f is_continuous_in x0 implies x0 in dom f & for s1 be sequence of S st
rng s1 c= dom f & s1 is convergent & lim s1=x0 &
(for n being Nat holds s1.n<>x0) holds f
/*s1 is convergent & f/.x0=lim(f/*s1);
assume that
A1: x0 in dom f and
A2: for s1 st rng s1 c=dom f & s1 is convergent & lim s1=x0 & (for n being Nat
holds s1.n<>x0) holds f/*s1 is convergent & f/.x0=lim(f/*s1);
thus x0 in dom f by A1;
let s2 be sequence of S such that
A3: rng s2 c=dom f and
A4: s2 is convergent & lim s2=x0;
now
per cases;
suppose
ex n st for m be Element of NAT st n<=m holds s2.m=x0;
then consider N be Element of NAT such that
A5: for m be Element of NAT st N<=m holds s2.m=x0;
A6: for n holds (s2^\N).n=x0
proof
let n;
s2.(n+N)=x0 by A5,NAT_1:12;
hence thesis by NAT_1:def 3;
end;
A7: rng (s2^\N) c= rng s2 by VALUED_0:21;
A8: now
let p be Real such that
A9: p>0;
reconsider n=0 as Nat;
take n;
let m be Nat such that
n<=m;
A10: m in NAT by ORDINAL1:def 12;
||.(f/*(s2^\N)).m-f/.x0.|| =||.f/.((s2^\N).m)-f/.x0.|| by A3,A7,
FUNCT_2:109,XBOOLE_1:1,A10
.=||.f/.x0-f/.x0.|| by A6,A10
.=||.0.T.|| by RLVECT_1:15
.=0 by NORMSP_1:1;
hence ||.(f/*(s2^\N)).m-f/.x0.||< p by A9;
end;
then
A11: f/*(s2^\N) is convergent;
A12: f/*(s2^\N)=(f/*s2)^\N by A3,VALUED_0:27;
then
A13: f/*s2 is convergent by A11,LOPBAN_3:10;
f/.x0=lim((f/*s2)^\N) by A8,A11,A12,NORMSP_1:def 7;
hence thesis by A13,LOPBAN_3:9;
end;
suppose
A14: for n ex m be Element of NAT st n<=m & s2.m<>x0;
defpred P[Nat,set,set] means for n,m be Element of NAT st $2=
n & $3=m holds n<m & s2.m<>x0 & for k st n<k & s2.k<>x0 holds m<=k;
defpred P[Nat] means s2.$1<>x0;
ex m1 be Element of NAT st 0<=m1 & s2.m1<>x0 by A14;
then
A15: ex m be Nat st P[m];
consider M be Nat such that
A16: P[M] & for n be Nat st P[n] holds M<=n from NAT_1:sch 5(A15);
reconsider M9 = M as Element of NAT by ORDINAL1:def 12;
A17: now
let n;
consider m be Element of NAT such that
A18: n+1<=m & s2.m<>x0 by A14;
take m;
thus n<m & s2.m<>x0 by A18,NAT_1:13;
end;
A19: for n being Nat
for x be Element of NAT ex y be Element of NAT st P[n,x,y]
proof
let n be Nat;
let x be Element of NAT;
defpred P[Nat] means x<$1 & s2.$1<>x0;
ex m be Element of NAT st P[m] by A17;
then
A20: ex m be Nat st P[m];
consider l be Nat such that
A21: P[l] & for k be Nat st P[k] holds l<=k from NAT_1:sch 5(A20);
reconsider l as Element of NAT by ORDINAL1:def 12;
take l;
thus thesis by A21;
end;
consider F be sequence of NAT such that
A22: F.0=M9 & for n be Nat holds P[n,F.n,F.(n+1)] from
RECDEF_1:sch 2(A19);
A23: rng F c= REAL by NUMBERS:19;
A24: rng F c= NAT;
A25: dom F=NAT by FUNCT_2:def 1;
then reconsider F as Real_Sequence by A23,RELSET_1:4;
A26: now
let n;
F.n in rng F by A25,FUNCT_1:def 3;
hence F.n is Element of NAT by A24;
end;
now
let n be Nat;
A27: n in NAT by ORDINAL1:def 12;
F.n is Element of NAT & F.(n+1) is Element of NAT by A26,A27;
hence F.n<F.(n+1) by A22;
end;
then reconsider F as increasing sequence of NAT by SEQM_3:def 6;
A28: s2*F is convergent & lim (s2*F)=x0 by A4,LOPBAN_3:7,8;
A29: for n st s2.n<>x0 ex m be Element of NAT st F.m=n
proof
defpred P[Nat] means s2.$1<>x0 & for m be Element of NAT holds F.m<>$1;
assume ex n st P[n];
then
A30: ex n be Nat st P[n];
consider M1 be Nat such that
A31: P[M1] & for n be Nat st P[n] holds M1<=n from NAT_1:sch 5(A30
);
defpred P[Nat] means $1<M1 & s2.$1<>x0 & ex m be Element of NAT st F.m
=$1;
A32: ex n be Nat st P[n]
proof
take M;
M<=M1 & M <> M1 by A16,A22,A31;
hence M<M1 by XXREAL_0:1;
thus s2.M<>x0 by A16;
take 0;
thus thesis by A22;
end;
A33: for n be Nat st P[n] holds n<=M1;
consider MX be Nat such that
A34: P[MX] & for n be Nat st P[n] holds n<=MX from NAT_1:sch 6(A33
,A32);
A35: for k st MX<k & k<M1 holds s2.k=x0
proof
given k such that
A36: MX<k and
A37: k<M1 & s2.k<>x0;
now
per cases;
suppose
ex m be Element of NAT st F.m=k;
hence contradiction by A34,A36,A37;
end;
suppose
for m be Element of NAT holds F.m<>k;
hence contradiction by A31,A37;
end;
end;
hence contradiction;
end;
consider m be Element of NAT such that
A38: F.m=MX by A34;
A39: MX<F.(m+1) & s2.(F.(m+1))<>x0 by A22,A38;
M1 in NAT by ORDINAL1:def 12;
then
A40: F.(m+1)<=M1 by A22,A31,A34,A38;
now
assume F.(m+1)<>M1;
then F.(m+1)<M1 by A40,XXREAL_0:1;
hence contradiction by A35,A39;
end;
hence contradiction by A31;
end;
A41: for n being Nat holds (s2*F).n<>x0
proof
defpred P[Nat] means (s2*F).$1<>x0;
A42: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
(s2*F).k<>x0;
P[k,F.k,F.(k+1)] by A22;
then s2.(F.(k+1))<>x0;
hence thesis by FUNCT_2:15;
end;
A43: P[0] by A16,A22,FUNCT_2:15;
thus for n being Nat holds P[n] from NAT_1:sch 2(A43,A42);
end;
A44: rng (s2*F) c= rng s2 by VALUED_0:21;
then rng (s2*F) c= dom f by A3;
then
A45: f/*(s2*F) is convergent & f/.x0=lim(f/*(s2*F)) by A2,A41,A28;
A46: now
let p be Real;
assume
A47: 0<p;
then consider n being Nat such that
A48: for m be Nat st n<=m holds ||.(f/*(s2*F)).m-f/.x0
.||<p by A45,NORMSP_1:def 7;
reconsider k=F.n as Nat;
take k;
let m be Nat such that
A49: k<=m;
A50: m in NAT by ORDINAL1:def 12;
now
per cases;
suppose
A51: s2.m=x0;
||.(f/*s2).m-f/.x0.|| =||.f/.(s2.m)-f/.x0.|| by A3,FUNCT_2:109,A50
.=||.0.T.|| by A51,RLVECT_1:15
.=0 by NORMSP_1:1;
hence ||.(f/*s2).m-f/.x0.||<p by A47;
end;
suppose
s2.m<>x0;
then consider l be Element of NAT such that
A52: m=F.l by A29,A50;
n<=l by A49,A52,SEQM_3:1;
then ||.(f/*(s2*F)).l-f/.x0.||<p by A48;
then ||.f/.((s2*F).l)-f/.x0.||<p by A3,A44,FUNCT_2:109,XBOOLE_1:1;
then ||.f/.(s2.m)-f/.x0.||<p by A52,FUNCT_2:15;
hence ||.(f/*s2).m-f/.x0.||<p by A3,FUNCT_2:109,A50;
end;
end;
hence ||.(f/*s2).m-f/.x0.||<p;
end;
hence f/*s2 is convergent;
hence f/.x0=lim(f/*s2) by A46,NORMSP_1:def 7;
end;
end;
hence thesis;
end;
theorem Th28:
for R1,R2 holds R1+R2 is RestFunc of S,T & R1-R2 is RestFunc of S,T
proof
let R1,R2;
A1: R1 is total & R2 is total by Def5;
A2: now
let h ;
assume A3: h is non-zero;
A4: (||.h.||")(#)(R1/*h) is convergent & (||.h.||")(#)(R2/*h) is
convergent by Def5,A3;
A5: (||.h.||")(#)((R1+R2)/*h) = (||.h.||")(#)((R1/*h)+(R2/*h)) by A1,Th25
.= ((||.h.||")(#)(R1/*h))+((||.h.||")(#)(R2/*h)) by Th9;
hence (||.h.||")(#)((R1+R2)/*h) is convergent by A4,NORMSP_1:19;
lim ((||.h.||")(#)(R1/*h)) = 0.T & lim ((||.h.||")(#)(R2/*h)) = 0.T
by A3,Def5;
hence lim ((||.h.||")(#)((R1+R2)/*h)) = 0.T+0.T by A4,A5,NORMSP_1:25
.= 0.T by RLVECT_1:4;
end;
A6: now
let h;
assume A7: h is non-zero;
A8: (||.h.||")(#)(R1/*h) is convergent & (||.h.||")(#)(R2/*h) is
convergent by Def5,A7;
A9: (||.h.||")(#)((R1-R2)/*h) = (||.h.||")(#)((R1/*h)-(R2/*h)) by A1,Th25
.= ((||.h.||")(#)(R1/*h))-((||.h.||")(#)(R2/*h)) by Th12;
hence (||.h.||")(#)((R1-R2)/*h) is convergent by A8,NORMSP_1:20;
lim ((||.h.||")(#)(R1/*h)) = 0.T & lim ((||.h.||")(#)(R2/*h)) = 0.T
by Def5,A7;
hence lim ((||.h.||")(#)((R1-R2)/*h)) = 0.T-0.T by A8,A9,NORMSP_1:26
.= 0.T by RLVECT_1:13;
end;
R1+R2 is total by A1,VFUNCT_1:32;
hence R1+R2 is RestFunc of S,T by A2,Def5;
R1-R2 is total by A1,VFUNCT_1:32;
hence thesis by A6,Def5;
end;
theorem Th29:
for r,R holds r(#)R is RestFunc of S,T
proof
let r,R;
A1: R is total by Def5;
A2: now
let h;
assume A3: h is non-zero;
A4: (||.h.||")(#)(R/*h) is convergent by A3,Def5;
A5: (||.h.||")(#)((r(#)R)/*h) = (||.h.||")(#)(r*(R/*h)) by A1,Th26
.= r*((||.h.||")(#)(R/*h)) by Th10;
hence (||.h.||")(#)((r(#)R)/*h) is convergent by A4,NORMSP_1:22;
lim ((||.h.||")(#)(R/*h)) = 0.T by A3,Def5;
hence lim ((||.h.||")(#)((r(#)R)/*h)) = r*0.T by A4,A5,NORMSP_1:28
.= 0.T by RLVECT_1:10;
end;
r(#)R is total by A1,VFUNCT_1:34;
hence thesis by A2,Def5;
end;
definition
let S,T;
let f be PartFunc of S,T;
let x0 be Point of S;
pred f is_differentiable_in x0 means
ex N being Neighbourhood of x0
st N c= dom f & ex L,R st for x be Point of S st x in N holds f/.x - f/.x0 = L.
(x-x0) + R/.(x-x0);
end;
definition
let S,T;
let f be PartFunc of S,T;
let x0 be Point of S;
assume
A1: f is_differentiable_in x0;
func diff(f,x0) -> Point of R_NormSpace_of_BoundedLinearOperators(S,T) means
:Def7:
ex N being Neighbourhood of x0 st N c= dom f & ex R st for x be Point of
S st x in N holds f/.x-f/.x0 = it.(x-x0) + R/.(x-x0);
existence
by A1;
uniqueness
proof
let LB,LB1 be Point of R_NormSpace_of_BoundedLinearOperators(S,T);
A2: R_NormSpace_of_BoundedLinearOperators(S,T) = NORMSTR (#
BoundedLinearOperators(S,T), Zero_(BoundedLinearOperators(S,T),
R_VectorSpace_of_LinearOperators(S,T)), Add_(BoundedLinearOperators(S,T),
R_VectorSpace_of_LinearOperators(S,T)), Mult_(BoundedLinearOperators(S,T),
R_VectorSpace_of_LinearOperators(S,T)), BoundedLinearOperatorsNorm(S,T) #) by
LOPBAN_1:def 14;
then reconsider L = LB as Element of BoundedLinearOperators(S,T);
reconsider L1=LB1 as Element of BoundedLinearOperators(S,T) by A2;
assume that
A3: ex N being Neighbourhood of x0 st N c= dom f & ex R st for x be
Point of S st x in N holds f/.x-f/.x0 = LB.(x-x0)+R/.(x-x0) and
A4: ex N being Neighbourhood of x0 st N c= dom f & ex R st for x be
Point of S st x in N holds f/.x-f/.x0 = LB1.(x-x0) + R/.(x-x0);
consider N being Neighbourhood of x0 such that
N c= dom f and
A5: ex R st for x be Point of S st x in N holds f/.x-f/.x0 = LB.(x-x0)
+R /.(x-x0) by A3;
consider R such that
A6: for x be Point of S st x in N holds f/.x-f/.x0 = LB.(x-x0) + R/.(x
-x0) by A5;
consider N1 being Neighbourhood of x0 such that
N1 c= dom f and
A7: ex R st for x be Point of S st x in N1 holds f/.x-f/.x0=LB1.(x-x0
)+ R/.(x-x0) by A4;
consider R1 such that
A8: for x be Point of S st x in N1 holds f/.x-f/.x0 = LB1.(x-x0) + R1
/.(x-x0) by A7;
A9: for z be Point of S holds modetrans(L,S,T).z = modetrans(L1,S,T).z
proof
let z be Point of S;
now
per cases;
case
A10: z= 0.S;
hence modetrans(L,S,T).z =modetrans(L,S,T).(0*z) by RLVECT_1:10
.=0*modetrans(L,S,T).z by LOPBAN_1:def 5
.=0.T by RLVECT_1:10
.=0*modetrans(L1,S,T).z by RLVECT_1:10
.=modetrans(L1,S,T).(0*z) by LOPBAN_1:def 5
.=modetrans(L1,S,T).z by A10,RLVECT_1:10;
end;
case
A11: z<> 0.S;
consider N0 be Neighbourhood of x0 such that
A12: N0 c= N & N0 c= N1 by Th1;
consider g be Real such that
A13: 0<g and
A14: {y where y is Point of S: ||.y - x0 .|| < g} c= N0 by NFCONT_1:def 1;
consider n0 be Nat such that
A15: ||.z.|| /g < n0 by SEQ_4:3;
set n1=n0+1;
n0 <= n0+1 by NAT_1:11;
then ||.z.|| /g < (n0+1) by A15,XXREAL_0:2;
then ( ||.z.|| /g)*g < (n0+1)*g by A13,XREAL_1:68;
then ||.z.|| < (n0+1)*g by A13,XCMPLX_1:87;
then
A16: ||.z.|| /(n0+1) < g by XREAL_1:83;
ex r be Real_Sequence st (for n be Element of NAT holds (r.n=1
/(n+n1) & r.n > 0 & r.n*z+x0 in N0) ) & r is convergent & lim r =0
proof
deffunc F(Nat) = 1 /($1+n1);
consider r be Real_Sequence such that
A17: for n being Nat holds r.n = F(n) from SEQ_1:sch 1;
take r;
thus for n be Element of NAT holds r.n=1 /(n+n1) & r.n > 0 & r.n*z
+x0 in N0
proof
let n be Element of NAT;
thus r.n=1 /(n+n1) by A17;
n1 <= n+n1 & 0 <= ||.z.|| by NAT_1:12,NORMSP_1:4;
then
A18: ||.z.|| /(n+n1) <= ||.z.|| /n1 by XREAL_1:118;
0 < 1 * (n + n1)";
then
0 < 1/(n + n1) by XCMPLX_0:def 9;
hence r.n >0 by A17;
||.r.n*z+x0-x0.|| = ||.r.n*z+(x0-x0).|| by RLVECT_1:def 3
.= ||.r.n*z+0.S.|| by RLVECT_1:15
.= ||.r.n*z.|| by RLVECT_1:4
.= ||.(1 /(n+n1))*z.|| by A17
.= |.1 /(n+n1).|* ||.z.|| by NORMSP_1:def 1
.= ( 1 /(n+n1) )* ||.z.|| by ABSVALUE:def 1
.= ||.z.|| /(n+n1) by XCMPLX_1:99;
then ||.r.n*z+x0-x0.|| < g by A16,A18,XXREAL_0:2;
then (r.n*z+x0) in {y where y is Point of S: ||.y - x0 .|| < g};
hence thesis by A14;
end;
thus thesis by A17,SEQ_4:31;
end;
then consider r be Real_Sequence such that
A19: for n be Element of NAT holds r.n=1 /(n+n1) & r.n > 0 & r.n
*z+x0 in N0 and
r is convergent and
lim r =0;
deffunc F(Element of NAT) = r.$1*z;
consider s be sequence of S such that
A20: for n holds s.n = F(n) from FUNCT_2:sch 4;
now
let n be Nat;
A21: n in NAT by ORDINAL1:def 12;
assume s.n = 0.S;
then r.n*z = 0.S by A20,A21;
then r.n =0 or z=0.S by RLVECT_1:11;
hence contradiction by A11,A19,A21;
end;
then
A22: s is non-zero by Th7;
now
let n be Nat;
A23: n in NAT by ORDINAL1:def 12;
hence s.n = r.n*z by A20
.=(1 /(n+n1))*z by A19,A23;
end;
then s is convergent & lim s = 0.S by Th19,Th20;
then reconsider s as (0.S)-convergent sequence of S
by Def4;
A24: now
let x be Point of S;
assume that
A25: x in N and
A26: x in N1;
f/.x-f/.x0 = L.(x-x0) + R/.(x-x0) by A6,A25;
hence L.(x-x0) + R/.(x-x0) = L1.(x-x0) + R1/.(x-x0) by A8,A26;
end;
now
R1 is total by Def5;
then dom R1 = the carrier of S by PARTFUN1:def 2;
then
A27: rng s c= dom R1;
R is total by Def5;
then dom R = the carrier of S by PARTFUN1:def 2;
then
A28: rng s c= dom R;
let n be Nat;
set x=(r.n)*z+x0;
A29: x-x0 = (r.n)*z+(x0 -x0) by RLVECT_1:def 3
.= (r.n)*z+0.S by RLVECT_1:15
.=(r.n)*z by RLVECT_1:4;
A30: n in NAT by ORDINAL1:def 12;
then
A31: r.n <> 0 by A19;
s.n <> 0.S by A22,Th7;
then
A32: ||.s.n.|| <> 0 by NORMSP_0:def 5;
A33: r.n > 0 by A19,A30;
||.s.n.|| = ||.(r.n)*z.|| by A20,A30
.= |.r.n.| * ||.z.|| by NORMSP_1:def 1
.=r.n * ||.z.|| by A33,ABSVALUE:def 1;
then (r.n)"* ||.s.n.|| = (r.n)"* r.n * ||.z.||
.= ((r.n)/(r.n))* ||.z.|| by XCMPLX_0:def 9
.= 1* ||.z.|| by A31,XCMPLX_1:60
.= ||.z.||;
then
||.z.|| *( ||.s.n.|| )" = (r.n)"* (||.s.n.|| *( ||.s.n.|| )")
.= (r.n)"* (||.s.n.|| /( ||.s.n.|| )) by XCMPLX_0:def 9
.= (r.n)"*1 by A32,XCMPLX_1:60
.= (r.n)";
then
A34: ||.z.|| *( ||.s.||.n )" = (r.n)" by NORMSP_0:def 4;
x in N0 by A19,A30;
then
L.((r.n)*z) + R/.((r.n)*z) = L1.((r.n)*z) + R1/.(( r.n)*z) by A24
,A12,A29;
then
A35: (r.n)"*(L.((r.n)*z))+(r.n)"*(R/.((r.n)*z)) =(r.n)"*(L1.((r.n)
*z)+R1/.((r.n)*z)) by RLVECT_1:def 5;
A36: (r.n)"*(L1.((r.n)*z)) =(r.n)"*(modetrans(L1,S,T).((r.n)*z))
by LOPBAN_1:def 11
.=(r.n)"*((r.n)*modetrans(L1,S,T).z) by LOPBAN_1:def 5
.= (r.n)"*((r.n)*L1.z ) by LOPBAN_1:def 11
.= ((r.n)"*(r.n))*L1.z by RLVECT_1:def 7
.= ((r.n)/(r.n))*L1.z by XCMPLX_0:def 9
.= 1*L1.z by A31,XCMPLX_1:60
.= L1.z by RLVECT_1:def 8;
(r.n)"*(L.((r.n)*z)) =(r.n)"*(modetrans(L,S,T).((r.n)*z)) by
LOPBAN_1:def 11
.=(r.n)"*((r.n)*modetrans(L,S,T).z) by LOPBAN_1:def 5
.= (r.n)"*((r.n)*L.z ) by LOPBAN_1:def 11
.= ((r.n)"*(r.n))*L.z by RLVECT_1:def 7
.= ((r.n)/(r.n))*L.z by XCMPLX_0:def 9
.= 1*L.z by A31,XCMPLX_1:60
.= L.z by RLVECT_1:def 8;
then
A37: L.z + (r.n)" *(R/.((r.n)*z)) = L1.z + (r.n)"*(R1/. ((r.n)*z))
by A35,A36,RLVECT_1:def 5;
A38: (r.n)"*(R1/.((r.n)*z)) = (r.n)"*(R1/.(s.n)) by A20,A30
.= ( ||.z.|| *||.s.||".n)*(R1/.(s.n)) by A34,VALUED_1:10
.= ||.z.|| *(||.s.||".n *(R1/.(s.n)) ) by RLVECT_1:def 7
.= ||.z.|| *((||.s.||".n)*((R1/*s).n)) by A30,A27,FUNCT_2:109
.= ||.z.|| *((||.s.||")(#)(R1/*s)).n by Def2;
(r.n)"*(R/.((r.n)*z)) = (r.n)"*(R/.(s.n)) by A20,A30
.= ( ||.z.|| *||.s.||".n)*(R/.(s.n)) by A34,VALUED_1:10
.= ||.z.|| *(||.s.||".n *(R/.(s.n)) ) by RLVECT_1:def 7
.= ||.z.|| *((||.s.||".n)*((R/*s).n)) by A30,A28,FUNCT_2:109
.= ||.z.|| *((||.s.||")(#)(R/*s)).n by Def2;
then L.z + ( ||.z.|| *((||.s.||")(#)(R/*s)).n -( ||.z.|| *((||.s
.||")(#)(R/*s)).n)) = L1.z + ||.z.|| *((||.s.||")(#)(R1/*s)).n -(||.z.|| *((||.
s.||")(#)(R/*s)).n) by A37,A38,RLVECT_1:def 3;
then L.z + 0.T = L1.z + ||.z.|| *((||.s.||")(#)(R1/*s)).n -(||.z
.|| *((||.s.||")(#)(R/*s)).n) by RLVECT_1:15;
then L.z = L1.z + ||.z.|| *((||.s.||")(#)(R1/*s)).n -(||.z.|| *((
||.s.||")(#)(R/*s)).n) by RLVECT_1:def 4;
then
L.z - L1.z = (- L1.z)+ (L1.z + ( ||.z.|| *((||.s.||")(#)(R1/*
s)).n -(||.z.|| *((||.s.||")(#)(R/*s)).n) )) by RLVECT_1:def 3;
then
L.z - L1.z = (- L1.z)+ L1.z + (||.z.|| *((||.s.||")(#)(R1/*s)
).n -(||.z.|| *((||.s.||")(#)(R/*s)).n) ) by RLVECT_1:def 3;
then L.z - L1.z = 0.T+ ( ||.z.|| *((||.s.||")(#)(R1/*s)).n -(||.z
.|| *((||.s.||")(#)(R/*s)).n) ) by RLVECT_1:5;
then
L.z - L1.z = (||.z.|| *((||.s.||")(#)(R1/*s)).n -(||.z.|| *((
||.s.||")(#)(R/*s)).n) ) by RLVECT_1:4;
then L.z - L1.z = ||.z.|| *((||.s.||"(#)(R1/*s)).n-(||.s.||"(#)(R
/*s)).n) by RLVECT_1:34;
then
L.z - L1.z = ||.z.|| *((||.s.||"(#)(R1/*s))-(||.s.||"(#)(R/*s
))).n by NORMSP_1:def 3;
hence L.z - L1.z = ( ||.z.|| *((||.s.||"(#)(R1/*s))-(||.s.||"(#)(R
/*s)))).n by NORMSP_1:def 5;
end;
then
||.z.|| *((||.s.||"(#)(R1/*s))-(||.s.||"(#)(R/*s))) is constant
& ( ||.z.|| *((||.s.||"(#)(R1/*s))-(||.s.||"(#)(R/*s)))).1 =L.z - L1.z by
VALUED_0:def 18;
then
A39: lim ( ||.z.|| *((||.s.||"(#)(R1/*s))-(||.s.||"(#)(R/*s)) )) = L
.z - L1.z by Th18;
A40: (||.s.||")(#)(R/*s) is convergent & (||.s.||")(#)(R1/*s) is
convergent by A22,Def5;
lim ((||.s.||")(#)(R/*s)) = 0.T & lim ((||.s.||")(#)(R1/*s)) =
0.T by A22,Def5;
then
A41: lim ((||.s.||"(#)(R1/*s))-(||.s.||"(#)(R/*s))) = 0.T - 0.T by A40,
NORMSP_1:26
.= 0.T by RLVECT_1:13;
A42: lim ( ||.z.|| *((||.s.||"(#)(R1/*s))-(||.s.||"(#)(R/*s)))) =
||.z.|| * lim ((||.s.||"(#)(R1/*s))-(||.s.||"(#)(R/*s))) by A40,NORMSP_1:20,28
.=0.T by A41,RLVECT_1:10;
thus modetrans(L,S,T).z =L.z by LOPBAN_1:def 11
.=L1.z by A39,A42,RLVECT_1:21
.= modetrans(L1,S,T).z by LOPBAN_1:def 11;
end;
end;
hence thesis;
end;
thus LB=modetrans(L,S,T) by LOPBAN_1:def 11
.=modetrans(L1,S,T) by A9,FUNCT_2:63
.=LB1 by LOPBAN_1:def 11;
end;
end;
definition
let X;
let S,T;
let f be PartFunc of S,T;
pred f is_differentiable_on X means
X c=dom f & for x be Point of S st x in X holds f|X is_differentiable_in x;
end;
theorem Th30:
for f be PartFunc of S,T holds (f is_differentiable_on X implies
X is Subset of S)
by XBOOLE_1:1;
theorem Th31:
for f be PartFunc of S,T for Z be Subset of S st Z is open holds
( f is_differentiable_on Z iff Z c=dom f & for x be Point of S st x in Z holds
f is_differentiable_in x )
proof
let f be PartFunc of S,T;
let Z be Subset of S such that
A1: Z is open;
thus f is_differentiable_on Z implies Z c=dom f & for x be Point of S st x
in Z holds f is_differentiable_in x
proof
assume
A2: f is_differentiable_on Z;
hence
A3: Z c=dom f;
let x0 be Point of S;
assume
A4: x0 in Z;
then f|Z is_differentiable_in x0 by A2;
then consider N being Neighbourhood of x0 such that
A5: N c= dom(f|Z) and
A6: ex L,R st for x be Point of S st x in N holds (f|Z)/.x-(f|Z)/.x0=L
.( x-x0)+R/.(x-x0);
consider L,R such that
A7: for x be Point of S st x in N holds (f|Z)/.x - (f|Z)/.x0 = L.(x-
x0) + R/.(x-x0) by A6;
take N;
A8: dom(f|Z)=dom f/\Z by RELAT_1:61;
then dom(f|Z) c=dom f by XBOOLE_1:17;
hence N c= dom f by A5;
take L,R;
let x be Point of S;
assume
A9: x in N;
then (f|Z)/.x-(f|Z)/.x0=L.(x-x0)+R/.(x-x0) by A7;
then f/.x-(f|Z)/.x0=L.(x-x0)+R/.(x-x0) by A5,A8,A9,PARTFUN2:16;
hence thesis by A3,A4,PARTFUN2:17;
end;
assume that
A10: Z c=dom f and
A11: for x be Point of S st x in Z holds f is_differentiable_in x;
thus Z c=dom f by A10;
let x0 be Point of S;
assume
A12: x0 in Z;
then consider N1 being Neighbourhood of x0 such that
A13: N1 c= Z by A1,Th2;
f is_differentiable_in x0 by A11,A12;
then consider N being Neighbourhood of x0 such that
A14: N c= dom f and
A15: ex L,R st for x be Point of S st x in N holds f/.x-f/.x0=L.(x-x0)+R
/.(x-x0);
consider N2 being Neighbourhood of x0 such that
A16: N2 c= N1 and
A17: N2 c= N by Th1;
A18: N2 c= Z by A13,A16;
take N2;
N2 c= dom f by A14,A17;
then
A19: N2 c= dom f/\Z by A18,XBOOLE_1:19;
hence N2 c= dom(f|Z) by RELAT_1:61;
A20: x0 in N2 by NFCONT_1:4;
consider L,R such that
A21: for x be Point of S st x in N holds f/.x-f/.x0=L.(x-x0)+R/.(x-x0) by A15;
take L,R;
let x be Point of S;
assume
A22: x in N2;
then f/.x-f/.x0=L.(x-x0)+R/.(x-x0) by A17,A21;
then (f|Z)/.x-f/.x0=L.(x-x0)+R/.(x-x0) by A19,A22,PARTFUN2:16;
hence thesis by A19,A20,PARTFUN2:16;
end;
theorem
for f be PartFunc of S,T for Y be Subset of S holds f
is_differentiable_on Y implies Y is open
proof
let f be PartFunc of S,T;
let Y be Subset of S;
assume
A1: f is_differentiable_on Y;
now
let x0 be Point of S;
assume x0 in Y;
then f|Y is_differentiable_in x0 by A1;
then consider N being Neighbourhood of x0 such that
A2: N c= dom(f|Y) and
ex L,R st for x be Point of S st x in N holds (f|Y)/.x-(f|Y)/.x0=L.( x
-x0)+R/.(x-x0);
take N;
dom(f|Y)=dom f/\Y by RELAT_1:61;
then dom(f|Y) c=Y by XBOOLE_1:17;
hence N c= Y by A2;
end;
hence thesis by Th4;
end;
definition
let S,T;
let f be PartFunc of S,T;
let X be set;
assume
A1: f is_differentiable_on X;
func f`|X -> PartFunc of S, R_NormSpace_of_BoundedLinearOperators(S,T) means
:Def9:
dom it = X & for x be Point of S st x in X holds it/.x = diff(f,x);
existence
proof
deffunc F(Point of S) = diff(f,$1);
defpred P[Point of S] means $1 in X;
consider F being PartFunc of S,R_NormSpace_of_BoundedLinearOperators(S,T)
such that
A2: (for x be Point of S holds x in dom F iff P[x]) & for x be Point
of S st x in dom F holds F.x = F(x) from SEQ_1:sch 3;
take F;
now
A3: X is Subset of S by A1,Th30;
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 being object st y in dom F holds y in X by A2;
then dom F c= X;
hence dom F = X by A4;
now
let x be Point of S;
assume x in X;
then
A5: x in dom F by A2;
then F.x = diff(f,x) by A2;
hence F/.x = diff(f,x) by A5,PARTFUN1:def 6;
end;
hence thesis;
end;
uniqueness
proof
let F,G be PartFunc of S,R_NormSpace_of_BoundedLinearOperators(S,T);
assume that
A6: dom F = X and
A7: for x be Point of S st x in X holds F/.x = diff(f,x) and
A8: dom G = X and
A9: for x be Point of S st x in X holds G/.x = diff(f,x);
now
let x be Point of S;
assume
A10: x in dom F;
then F/.x = diff(f,x) by A6,A7;
hence F/.x=G/.x by A6,A9,A10;
end;
hence thesis by A6,A8,PARTFUN2:1;
end;
end;
theorem
for f be PartFunc of S,T for Z be Subset of S st Z is open & Z c= dom
f & ex r be Point of T st rng f = {r} holds f is_differentiable_on Z & for x be
Point of S st x in Z holds (f`|Z)/.x = 0.R_NormSpace_of_BoundedLinearOperators(
S,T)
proof
let f be PartFunc of S,T;
let Z be Subset of S such that
A1: Z is open and
A2: Z c= dom f;
reconsider R = (the carrier of S) --> 0.T as PartFunc of S,T;
set L = 0.R_NormSpace_of_BoundedLinearOperators(S,T);
given r be Point of T such that
A3: rng f = {r};
R_NormSpace_of_BoundedLinearOperators(S,T) = NORMSTR (#
BoundedLinearOperators(S,T), Zero_(BoundedLinearOperators(S,T),
R_VectorSpace_of_LinearOperators(S,T)), Add_(BoundedLinearOperators(S,T),
R_VectorSpace_of_LinearOperators(S,T)), Mult_(BoundedLinearOperators(S,T),
R_VectorSpace_of_LinearOperators(S,T)), BoundedLinearOperatorsNorm(S,T) #) by
LOPBAN_1:def 14;
then reconsider L as Element of BoundedLinearOperators(S,T);
A4: dom R = the carrier of S;
A5: now
let h;
assume h is non-zero;
A6: now
let n be Nat;
A7: R/.(h.n) =R.(h.n) by A4,PARTFUN1:def 6
.=0.T;
A8: rng h c= dom R;
A9: n in NAT by ORDINAL1:def 12;
thus ((||.h.||")(#)(R/*h)).n = (||.h.||".n)*((R/*h).n) by Def2
.= (||.h.||".n)*(R/.(h.n)) by A9,A8,FUNCT_2:109
.= 0.T by A7,RLVECT_1:10;
end;
then
A10: (||.h.||")(#)(R/*h) is constant by VALUED_0:def 18;
hence (||.h.||")(#)(R/*h) is convergent by Th18;
((||.h.||")(#)(R/*h)).0 = 0.T by A6;
hence lim ((||.h.||")(#)(R/*h)) = 0.T by A10,Th18;
end;
A11: now
let x0 be Point of S;
assume
A12: x0 in dom f;
then f.x0 in {r} by A3,FUNCT_1:def 3;
then f/.x0 in {r} by A12,PARTFUN1:def 6;
hence f/.x0 = r by TARSKI:def 1;
end;
reconsider R as RestFunc of S,T by A5,Def5;
A13: ((the carrier of S) --> 0.T) = L by LOPBAN_1:31;
A14: now
let x0 be Point of S;
assume
A15: x0 in Z;
then consider N being Neighbourhood of x0 such that
A16: N c= Z by A1,Th2;
A17: N c= dom f by A2,A16;
for x be Point of S st x in N holds f/.x - f/.x0 = L.(x-x0) + R/.(x- x0)
proof
let x be Point of S;
A18: R/.(x-x0) =R.(x-x0) by A4,PARTFUN1:def 6
.=0.T;
assume x in N;
hence f/.x - f/.x0 = r - f/.x0 by A11,A17
.= r - r by A2,A11,A15
.=0.T by RLVECT_1:15
.= 0.T + 0.T by RLVECT_1:4
.= L.(x-x0)+R/.(x-x0) by A13,A18;
end;
hence f is_differentiable_in x0 by A17;
end;
hence
A19: f is_differentiable_on Z by A1,A2,Th31;
let x0 be Point of S;
assume
A20: x0 in Z;
then
A21: f is_differentiable_in x0 by A14;
then
ex N being Neighbourhood of x0 st N c= dom f & ex L,R st for x be Point
of S st x in N holds f/.x-f/.x0=L.(x-x0)+R/.(x-x0);
then consider N being Neighbourhood of x0 such that
A22: N c= dom f;
A23: for x be Point of S st x in N holds f/.x - f/.x0 = L.(x-x0) + R/.(x-x0)
proof
let x be Point of S;
A24: R/.(x-x0) =R.(x-x0) by A4,PARTFUN1:def 6
.=0.T;
assume x in N;
hence f/.x - f/.x0 = r - f/.x0 by A11,A22
.=r - r by A2,A11,A20
.=0.T by RLVECT_1:15
.= 0.T + 0.T by RLVECT_1:4
.=L.(x-x0) + R/.(x-x0) by A13,A24;
end;
thus (f`|Z)/.x0 = diff(f,x0) by A19,A20,Def9
.= 0.R_NormSpace_of_BoundedLinearOperators(S,T) by A21,A22,A23,Def7;
end;
registration
let S;
let h,n;
cluster h^\n -> (0.S)-convergent for sequence of S;
coherence
proof
A1: h is convergent by Def4;
lim h = 0.S by Def4;
then
A2: lim (h^\n) = 0.S by A1,LOPBAN_3:9;
h^\n is convergent by A1,LOPBAN_3:9;
hence thesis by A2;
end;
end;
registration
let S be non trivial RealNormSpace;
let h be (0.S)-convergent non-zero sequence of S ;
let n;
cluster h^\n -> (0.S)-convergent non-zero for sequence of S;
coherence by Th17;
end;
theorem Th34:
for x0 be Point of S for N being Neighbourhood of x0 st f
is_differentiable_in x0 & N c= dom f holds
for h be (0.S)-convergent sequence of S st h is non-zero
holds
for c st rng c = {x0} & rng (h+c) c= N holds (f/*(h+c) - f/*c) is convergent
& lim (f/*(h+c) - f/*c) = 0.T
proof
let x0 be Point of S;
let N be Neighbourhood of x0;
assume that
A1: f is_differentiable_in x0 and
A2: N c= dom f;
let h be (0.S)-convergent sequence of S;
assume A3: h is non-zero;
let c such that
A4: rng c = {x0} and
A5: rng (h+c) c= N;
consider N1 be Neighbourhood of x0 such that
N1 c= dom f and
A6: ex L,R st for x be Point of S st x in N1 holds f/.x - f/.x0 = L.(x-
x0) + R/.(x-x0) by A1;
consider N2 be Neighbourhood of x0 such that
A7: N2 c= N and
A8: N2 c= N1 by Th1;
consider L,R such that
A9: for x be Point of S st x in N1 holds f/.x - f/.x0 = L.(x-x0) + R/.(x
-x0) by A6;
consider g be Real such that
A10: 0<g and
A11: {y where y is Point of S: ||.y-x0.|| < g} c= N2 by NFCONT_1:def 1;
A12: x0 in N2 by NFCONT_1:4;
ex n st rng (c^\n) c= N2 & rng ((h+c)^\n) c= N2
proof
c.0 in rng c by NFCONT_1:6;
then c.0=x0 by A4,TARSKI:def 1;
then
A13: lim c = x0 by Th18;
A14: c is convergent & h is convergent by Def4,Th18;
then
A15: h + c is convergent by NORMSP_1:19;
lim h = 0.S by Def4;
then lim (h + c) = 0.S + x0 by A13,A14,NORMSP_1:25
.= x0 by RLVECT_1:4;
then consider n being Nat such that
A16: for m being Nat st n<=m holds ||.(h+c).m-x0.||<g by A10,A15,
NORMSP_1:def 7;
reconsider n as Element of NAT by ORDINAL1:def 12;
take n;
A17: rng (c^\n) = {x0} by A4,VALUED_0:26;
thus rng (c^\n) c= N2
by A12,A17,TARSKI:def 1;
let y be object;
assume y in rng ((h+c)^\n);
then consider m be Nat such that
A18: y = ((h+c)^\n).m by NFCONT_1:6;
reconsider y1=y as Point of S by A18;
n + 0 <= n+m by XREAL_1:7;
then ||.(h+c).(n+m)-x0.||<g by A16;
then ||.((h+c)^\n).m - x0 .|| < g by NAT_1:def 3;
then y1 in {z where z is Point of S: ||.z-x0.|| < g} by A18;
hence thesis by A11;
end;
then consider n such that
rng (c^\n) c= N2 and
A19: rng ((h+c)^\n) c= N2;
A20: lim (h^\n) = 0.S by Def4;
A21: for k holds f/.(((h+c)^\n).k) - f/.((c^\n).k) = L.((h^\n).k) + R/.((h^\
n).k)
proof
let k;
((h+c)^\n).k in rng ((h+c)^\n) by NFCONT_1:6;
then
A22: ((h+c)^\n).k in N2 by A19;
(c^\n).k in rng (c^\n) & rng (c^\n) = rng c by NFCONT_1:6,VALUED_0:26;
then
A23: (c^\n).k = x0 by A4,TARSKI:def 1;
((h+c)^\n).k - (c^\n).k = (h+c).(k+n) - (c^\n).k by NAT_1:def 3
.=h.(k+n)+ c.(k+n) - (c^\n).k by NORMSP_1:def 2
.=(h^\n).k+ c.(k+n) - (c^\n).k by NAT_1:def 3
.=(h^\n).k+ (c^\n).k- (c^\n).k by NAT_1:def 3
.= (h^\n).k + ((c^\n).k - (c^\n).k) by RLVECT_1:def 3
.= (h^\n).k + 0.S by RLVECT_1:15
.= (h^\n).k by RLVECT_1:4;
hence thesis by A9,A8,A22,A23;
end;
R_NormSpace_of_BoundedLinearOperators(S,T) = NORMSTR (#
BoundedLinearOperators(S,T), Zero_(BoundedLinearOperators(S,T),
R_VectorSpace_of_LinearOperators(S,T)), Add_(BoundedLinearOperators(S,T),
R_VectorSpace_of_LinearOperators(S,T)), Mult_(BoundedLinearOperators(S,T),
R_VectorSpace_of_LinearOperators(S,T)), BoundedLinearOperatorsNorm(S,T) #) by
LOPBAN_1:def 14;
then reconsider L as Element of BoundedLinearOperators(S,T);
reconsider LP=modetrans(L,S,T) as PartFunc of S,T;
A24: h^\n is non-zero by A3,Th17;
then
A25: lim (R/*(h^\n)) = 0.T by Th24;
A26: rng ((h+c)^\n) c= dom f
by A19,A7,A2;
R is total by Def5;
then dom R = the carrier of S by PARTFUN1:def 2;
then
A27: rng (h^\n) c= dom R;
A28: rng (c^\n) c= dom f
proof
let y be object;
assume
A29: y in rng (c^\n);
rng (c^\n) = rng c by VALUED_0:26;
then y = x0 by A4,A29,TARSKI:def 1;
then y in N by NFCONT_1:4;
hence thesis by A2;
end;
A30: dom modetrans(L,S,T) = the carrier of S by FUNCT_2:def 1;
then
A31: rng (h^\n) c= dom modetrans(L,S,T);
now
let k;
thus (f/*((h+c)^\n)-f/*(c^\n)).k = (f/*((h+c)^\n)).k-(f/*(c^\n)).k by
NORMSP_1:def 3
.= f/.(((h+c)^\n).k) - (f/*(c^\n)).k by A26,FUNCT_2:109
.= f/.(((h+c)^\n).k) - f/.((c^\n).k) by A28,FUNCT_2:109
.= L.((h^\n).k) + R/.((h^\n).k) by A21
.= modetrans(L,S,T).((h^\n).k) + R/.((h^\n).k) by LOPBAN_1:def 11
.= LP/.((h^\n).k) + R/.((h^\n).k) by A30,PARTFUN1:def 6
.= (LP/*(h^\n)).k + R/.((h^\n).k) by A31,FUNCT_2:109
.= (LP/*(h^\n)).k + (R/*(h^\n)).k by A27,FUNCT_2:109
.= (LP/*(h^\n) + R/*(h^\n)).k by NORMSP_1:def 2;
end;
then
A32: f/*((h+c)^\n) - f/*(c^\n) = LP/*(h^\n) + R/*(h^\n) by FUNCT_2:63;
A33: dom modetrans(L,S,T) = the carrier of S by FUNCT_2:def 1;
LP is_Lipschitzian_on the carrier of S
proof
thus the carrier of S c=dom LP by FUNCT_2:def 1;
set LL=modetrans(L,S,T);
consider K being Real such that
A34: 0 <= K and
A35: for x being VECTOR of S holds ||. LL.x .|| <= K * ||. x .|| by
LOPBAN_1:def 8;
take K+1;
A36: 0 + K < 1 + K by XREAL_1:8;
now
let x1,x2 be Point of S such that
x1 in the carrier of S and
x2 in the carrier of S;
A37: ||.LL.(x1-x2) .|| <= K * ||.x1-x2.|| by A35;
0 <= ||.x1-x2.|| by NORMSP_1:4;
then
A38: K * ||.x1-x2.|| <= (K+1 ) * ||.x1-x2.|| by A36,XREAL_1:64;
||.LP/.x1-LP/.x2 .|| = ||.LL.x1-LP/.x2 .|| by A33,PARTFUN1:def 6
.= ||.LL.x1+-LL.x2 .|| by A33,PARTFUN1:def 6
.= ||.LL.x1+(-1)*LL.x2 .|| by RLVECT_1:16
.= ||.LL.x1+LL.((-1)*x2) .|| by LOPBAN_1:def 5
.= ||.LL.(x1+(-1)*x2) .|| by VECTSP_1:def 20
.= ||.LL.(x1-x2) .|| by RLVECT_1:16;
hence ||.LP/.x1-LP/.x2 .|| <= (K+1) * ||.x1-x2.|| by A37,A38,XXREAL_0:2;
end;
hence thesis by A34;
end;
then
A39: LP is_continuous_on the carrier of S by NFCONT_1:45;
A40: rng c c= dom f
proof
let y be object;
assume y in rng c;
then y = x0 by A4,TARSKI:def 1;
then y in N by NFCONT_1:4;
hence thesis by A2;
end;
A41: h^\n is convergent & rng (h^\n) c= the carrier of S by Def4;
then
A42: LP/*(h^\n) is convergent by A39,A20,NFCONT_1:18;
A43: R/*(h^\n) is convergent by A24,Th24;
then
A44: (LP/*(h^\n) + R/*(h^\n)) is convergent by A42,NORMSP_1:19;
LP/.(0.S) =modetrans(L,S,T).(0.S) by A33,PARTFUN1:def 6
.= modetrans(L,S,T).(0*0.S) by RLVECT_1:10
.=0*modetrans(L,S,T).0.S by LOPBAN_1:def 5
.=0.T by RLVECT_1:10;
then lim (LP/*(h^\n)) = 0.T by A39,A41,A20,NFCONT_1:18;
then lim (LP/*(h^\n) + R/*(h^\n)) = 0.T+0.T by A43,A25,A42,NORMSP_1:25;
then
A45: lim (LP/*(h^\n) + R/*(h^\n)) = 0.T by RLVECT_1:4;
rng (h+c) c= dom f
by A5,A2;
then f/*((h+c)^\n) - f/*(c^\n) =(f/*(h+c))^\n - f/*(c^\n) by VALUED_0:27
.=(f/*(h+c))^\n - (f/*c) ^\n by A40,VALUED_0:27
.= (f/*(h+c) - f/*c) ^\n by Th16;
hence thesis by A32,A44,A45,LOPBAN_3:10,11;
end;
theorem Th35:
for f1,f2,x0 st f1 is_differentiable_in x0 & f2
is_differentiable_in x0 holds f1+f2 is_differentiable_in x0 & diff(f1+f2,x0)=
diff(f1,x0)+diff(f2,x0)
proof
let f1,f2,x0;
assume that
A1: f1 is_differentiable_in x0 and
A2: f2 is_differentiable_in x0;
consider N1 be Neighbourhood of x0 such that
A3: N1 c= dom f1 and
A4: ex L,R st for x be Point of S st x in N1 holds f1/.x - f1/.x0 = L.(x
-x0) + R/.(x-x0) by A1;
consider L1,R1 such that
A5: for x be Point of S st x in N1 holds f1/.x - f1/.x0 = L1.(x-x0) + R1
/.(x-x0) by A4;
consider N2 be Neighbourhood of x0 such that
A6: N2 c= dom f2 and
A7: ex L,R st for x be Point of S st x in N2 holds f2/.x - f2/.x0 = L.(x
-x0) + R/.(x-x0) by A2;
consider L2,R2 such that
A8: for x be Point of S st x in N2 holds f2/.x - f2/.x0 = L2.(x-x0) + R2
/.(x-x0) by A7;
reconsider R=R1+R2 as RestFunc of S,T by Th28;
set L=L1+L2;
consider N be Neighbourhood of x0 such that
A9: N c= N1 and
A10: N c= N2 by Th1;
A11: N c= dom f2 by A6,A10;
N c= dom f1 by A3,A9;
then N /\ N c= dom f1 /\ dom f2 by A11,XBOOLE_1:27;
then
A12: N c= dom (f1+f2) by VFUNCT_1:def 1;
A13: R1 is total & R2 is total by Def5;
A14: now
let x be Point of S;
A15: x0 in N by NFCONT_1:4;
assume
A16: x in N;
hence (f1+f2)/.x - (f1+f2)/.x0 = (f1/.x+f2/.x) - (f1+f2)/.x0 by A12,
VFUNCT_1:def 1
.=f1/.x+f2/.x - (f1/.x0+f2/.x0) by A12,A15,VFUNCT_1:def 1
.=f1/.x+f2/.x - f1/.x0 - f2/.x0 by RLVECT_1:27
.=(f1/.x +-f1/.x0) + f2/.x - f2/.x0 by RLVECT_1:def 3
.=(f1/.x - f1/.x0) + (f2/.x - f2/.x0) by RLVECT_1:def 3
.=L1.(x-x0)+R1/.(x-x0) + (f2/.x - f2/.x0) by A5,A9,A16
.=L1.(x-x0)+R1/.(x-x0) + (L2.(x-x0) + R2/.(x-x0)) by A8,A10,A16
.=R1/.(x-x0)+L1.(x-x0) + L2.(x-x0) + R2/.(x-x0) by RLVECT_1:def 3
.=(L1.(x-x0)+L2.(x-x0)) + R1/.(x-x0) + R2/.(x-x0) by RLVECT_1:def 3
.=(L1.(x-x0)+L2.(x-x0)) + (R1/.(x-x0) + R2/.(x-x0)) by RLVECT_1:def 3
.=L.(x-x0)+(R1/.(x-x0) + R2/.(x-x0)) by LOPBAN_1:35
.=L.(x-x0)+R/.(x-x0) by A13,VFUNCT_1:37;
end;
hence f1+f2 is_differentiable_in x0 by A12;
hence diff(f1+f2,x0)=L by A12,A14,Def7
.=diff(f1,x0) + L2 by A1,A3,A5,Def7
.=diff(f1,x0) + diff(f2,x0) by A2,A6,A8,Def7;
end;
theorem Th36:
for f1,f2,x0 st f1 is_differentiable_in x0 & f2
is_differentiable_in x0 holds f1-f2 is_differentiable_in x0 & diff(f1-f2,x0)=
diff(f1,x0)-diff(f2,x0)
proof
let f1,f2,x0;
assume that
A1: f1 is_differentiable_in x0 and
A2: f2 is_differentiable_in x0;
consider N1 be Neighbourhood of x0 such that
A3: N1 c= dom f1 and
A4: ex L,R st for x be Point of S st x in N1 holds f1/.x - f1/.x0 = L.(x
-x0) + R/.(x-x0) by A1;
consider L1,R1 such that
A5: for x be Point of S st x in N1 holds f1/.x - f1/.x0 = L1.(x-x0) + R1
/.(x-x0) by A4;
consider N2 be Neighbourhood of x0 such that
A6: N2 c= dom f2 and
A7: ex L,R st for x be Point of S st x in N2 holds f2/.x - f2/.x0 = L.(x
-x0) + R/.(x-x0) by A2;
consider L2,R2 such that
A8: for x be Point of S st x in N2 holds f2/.x - f2/.x0 = L2.(x-x0) + R2
/.(x-x0) by A7;
reconsider R=R1-R2 as RestFunc of S,T by Th28;
set L=L1-L2;
consider N be Neighbourhood of x0 such that
A9: N c= N1 and
A10: N c= N2 by Th1;
A11: N c= dom f2 by A6,A10;
N c= dom f1 by A3,A9;
then N /\ N c= dom f1 /\ dom f2 by A11,XBOOLE_1:27;
then
A12: N c= dom (f1-f2) by VFUNCT_1:def 2;
A13: R1 is total & R2 is total by Def5;
A14: now
let x be Point of S;
A15: x0 in N by NFCONT_1:4;
assume
A16: x in N;
hence (f1-f2)/.x - (f1-f2)/.x0 = (f1/.x-f2/.x) - (f1-f2)/.x0 by A12,
VFUNCT_1:def 2
.=f1/.x - f2/.x - (f1/.x0-f2/.x0) by A12,A15,VFUNCT_1:def 2
.=f1/.x - f2/.x - f1/.x0 + f2/.x0 by RLVECT_1:29
.=f1/.x - (f1/.x0 + f2/.x) + f2/.x0 by RLVECT_1:27
.=f1/.x - f1/.x0 - f2/.x + f2/.x0 by RLVECT_1:27
.=f1/.x - f1/.x0 - (f2/.x - f2/.x0) by RLVECT_1:29
.=L1.(x-x0) + R1/.(x-x0) - (f2/.x - f2/.x0) by A5,A9,A16
.=L1.(x-x0) + R1/.(x-x0) - (L2.(x-x0) + R2/.(x-x0)) by A8,A10,A16
.=L1.(x-x0) + R1/.(x-x0) - L2.(x-x0) - R2/.(x-x0) by RLVECT_1:27
.=L1.(x-x0) + (R1/.(x-x0) +- L2.(x-x0)) - R2/.(x-x0) by RLVECT_1:def 3
.=L1.(x-x0) - (L2.(x-x0) - R1/.(x-x0)) - R2/.(x-x0) by RLVECT_1:33
.=L1.(x-x0) - L2.(x-x0) + R1/.(x-x0) - R2/.(x-x0) by RLVECT_1:29
.=L1.(x-x0) - L2.(x-x0) + (R1/.(x-x0) - R2/.(x-x0)) by RLVECT_1:def 3
.=L.(x-x0) + (R1/.(x-x0) - R2/.(x-x0)) by LOPBAN_1:40
.=L.(x-x0) + R/.(x-x0) by A13,VFUNCT_1:37;
end;
hence f1-f2 is_differentiable_in x0 by A12;
hence diff(f1-f2,x0)=L by A12,A14,Def7
.=diff(f1,x0) - L2 by A1,A3,A5,Def7
.=diff(f1,x0) - diff(f2,x0) by A2,A6,A8,Def7;
end;
theorem Th37:
for r,f,x0 st f is_differentiable_in x0 holds r(#)f
is_differentiable_in x0 & diff((r(#)f),x0) = r*diff(f,x0)
proof
let r,f,x0;
assume
A1: f is_differentiable_in x0;
then consider N1 be Neighbourhood of x0 such that
A2: N1 c= dom f and
A3: ex L,R st for x be Point of S st x in N1 holds f/.x - f/.x0 = L.(x-
x0) + R/.(x-x0);
consider L1,R1 such that
A4: for x be Point of S st x in N1 holds f/.x - f/.x0 = L1.(x-x0) + R1/.
(x-x0) by A3;
reconsider R = r(#)R1 as RestFunc of S,T by Th29;
set L = r*L1;
A5: N1 c= dom(r(#)f) by A2,VFUNCT_1:def 4;
A6: R1 is total by Def5;
A7: now
let x be Point of S;
A8: x0 in N1 by NFCONT_1:4;
assume
A9: x in N1;
hence (r(#)f)/.x - (r(#)f)/.x0 = r*(f/.x) - (r(#)f)/.x0 by A5,
VFUNCT_1:def 4
.= r*f/.x - r*f/.x0 by A5,A8,VFUNCT_1:def 4
.= r*(f/.x - f/.x0) by RLVECT_1:34
.= r*(L1.(x-x0) + R1/.(x-x0)) by A4,A9
.= r*L1.(x-x0) + r*R1/.(x-x0) by RLVECT_1:def 5
.= L.(x-x0) + r*R1/.(x-x0) by LOPBAN_1:36
.= L.(x-x0) + R/.(x-x0) by A6,VFUNCT_1:39;
end;
hence r(#)f is_differentiable_in x0 by A5;
hence diff((r(#)f),x0) = L by A5,A7,Def7
.= r*diff(f,x0) by A1,A2,A4,Def7;
end;
theorem
for f be PartFunc of S,S for Z be Subset of S st Z is open & Z c= dom
f & f|Z = id Z holds f is_differentiable_on Z & for x be Point of S st x in Z
holds (f`|Z)/.x = id (the carrier of S)
proof
set L= id (the carrier of S);
R_NormSpace_of_BoundedLinearOperators(S,S) = NORMSTR (#
BoundedLinearOperators(S,S), Zero_(BoundedLinearOperators(S,S),
R_VectorSpace_of_LinearOperators(S,S)), Add_(BoundedLinearOperators(S,S),
R_VectorSpace_of_LinearOperators(S,S)), Mult_(BoundedLinearOperators(S,S),
R_VectorSpace_of_LinearOperators(S,S)), BoundedLinearOperatorsNorm(S,S) #) & L
is Lipschitzian LinearOperator of S,S by LOPBAN_1:def 14,LOPBAN_2:3;
then reconsider L as Point of R_NormSpace_of_BoundedLinearOperators(S,S) by
LOPBAN_1:def 9;
let f be PartFunc of S,S;
let Z be Subset of S such that
A1: Z is open;
reconsider R = (the carrier of S) --> 0.S as PartFunc of S,S;
A2: dom R = (the carrier of S);
now
let h;
assume h is non-zero;
A3: now
let n be Nat;
A4: R/.(h.n) =R.(h.n) by A2,PARTFUN1:def 6
.=0.S;
A5: rng h c= dom R;
A6: n in NAT by ORDINAL1:def 12;
thus ((||.h.||")(#)(R/*h)).n = (||.h.||".n)*((R/*h).n) by Def2
.= (||.h.||".n)*(R/.(h.n)) by A6,A5,FUNCT_2:109
.= 0.S by A4,RLVECT_1:10;
end;
then
A7: (||.h.||")(#)(R/*h) is constant by VALUED_0:def 18;
hence (||.h.||")(#)(R/*h) is convergent by Th18;
((||.h.||")(#)(R/*h)).0 = 0.S by A3;
hence lim ((||.h.||")(#)(R/*h)) = 0.S by A7,Th18;
end;
then reconsider R as RestFunc of S,S by Def5;
assume that
A8: Z c= dom f and
A9: f|Z = id Z;
A10: now
let x be Point of S;
assume
A11: x in Z;
then f|Z.x = x by A9,FUNCT_1:18;
then f.x = x by A11,FUNCT_1:49;
hence f/.x =x by A8,A11,PARTFUN1:def 6;
end;
A12: now
let x0 be Point of S;
assume
A13: x0 in Z;
then consider N being Neighbourhood of x0 such that
A14: N c= Z by A1,Th2;
A15: for x be Point of S st x in N holds f/.x - f/.x0 = L.(x-x0) + R/.(x- x0)
proof
let x be Point of S;
A16: R/.(x-x0) =R.(x-x0) by A2,PARTFUN1:def 6
.=0.S;
assume x in N;
hence f/.x - f/.x0 = x - f/.x0 by A10,A14
.= x - x0 by A10,A13
.= L.(x-x0)
.= L.(x-x0) + R/.(x-x0) by A16,RLVECT_1:4;
end;
N c= dom f by A8,A14;
hence f is_differentiable_in x0 by A15;
end;
hence
A17: f is_differentiable_on Z by A1,A8,Th31;
let x0 be Point of S;
assume
A18: x0 in Z;
then consider N1 being Neighbourhood of x0 such that
A19: N1 c= Z by A1,Th2;
A20: f is_differentiable_in x0 by A12,A18;
then ex N being Neighbourhood of x0 st N c= dom f & ex L be Point of
R_NormSpace_of_BoundedLinearOperators(S,S),
R be RestFunc of S,S st for x be Point
of S st x in N holds f/.x - f/.x0 = L.(x-x0) + R/.(x-x0);
then consider N being Neighbourhood of x0 such that
A21: N c= dom f;
consider N2 being Neighbourhood of x0 such that
A22: N2 c= N1 and
A23: N2 c= N by Th1;
A24: N2 c= dom f by A21,A23;
A25: for x be Point of S st x in N2 holds f/.x - f/.x0 = L.(x-x0) + R/.(x-x0 )
proof
let x be Point of S;
A26: R/.(x-x0) =R.(x-x0) by A2,PARTFUN1:def 6
.=0.S;
assume x in N2;
then x in N1 by A22;
hence f/.x - f/.x0 = x - f/.x0 by A10,A19
.= x - x0 by A10,A18
.= L.(x-x0)
.= L.(x-x0) + R/.(x-x0) by A26,RLVECT_1:4;
end;
thus (f`|Z)/.x0 = diff(f,x0) by A17,A18,Def9
.= id the carrier of S by A20,A24,A25,Def7;
end;
theorem
for Z be Subset of S st Z is open for f1,f2 st Z c= dom (f1+f2) & f1
is_differentiable_on Z & f2 is_differentiable_on Z holds f1+f2
is_differentiable_on Z & for x be Point of S st x in Z holds ((f1+f2)`|Z)/.x =
diff(f1,x) + diff(f2,x)
proof
let Z be Subset of S such that
A1: Z is open;
let f1,f2;
assume that
A2: Z c= dom (f1+f2) and
A3: f1 is_differentiable_on Z & f2 is_differentiable_on Z;
now
let x0 be Point of S;
assume x0 in Z;
then f1 is_differentiable_in x0 & f2 is_differentiable_in x0 by A1,A3,Th31;
hence f1+f2 is_differentiable_in x0 by Th35;
end;
hence
A4: f1+f2 is_differentiable_on Z by A1,A2,Th31;
now
let x be Point of S;
assume
A5: x in Z;
then
A6: f1 is_differentiable_in x & f2 is_differentiable_in x by A1,A3,Th31;
thus ((f1+f2)`|Z)/.x = diff((f1+f2),x) by A4,A5,Def9
.= diff(f1,x) + diff(f2,x) by A6,Th35;
end;
hence thesis;
end;
theorem
for Z be Subset of S st Z is open for f1,f2 st Z c= dom (f1-f2) & f1
is_differentiable_on Z & f2 is_differentiable_on Z holds f1-f2
is_differentiable_on Z & for x be Point of S st x in Z holds ((f1-f2)`|Z)/.x =
diff(f1,x) - diff(f2,x)
proof
let Z be Subset of S such that
A1: Z is open;
let f1,f2;
assume that
A2: Z c= dom (f1-f2) and
A3: f1 is_differentiable_on Z & f2 is_differentiable_on Z;
now
let x0 be Point of S;
assume x0 in Z;
then f1 is_differentiable_in x0 & f2 is_differentiable_in x0 by A1,A3,Th31;
hence f1-f2 is_differentiable_in x0 by Th36;
end;
hence
A4: f1-f2 is_differentiable_on Z by A1,A2,Th31;
now
let x be Point of S;
assume
A5: x in Z;
then
A6: f1 is_differentiable_in x & f2 is_differentiable_in x by A1,A3,Th31;
thus ((f1-f2)`|Z)/.x = diff((f1-f2),x) by A4,A5,Def9
.= diff(f1,x) - diff(f2,x) by A6,Th36;
end;
hence thesis;
end;
theorem
for Z be Subset of S st Z is open for r,f st Z c= dom (r(#)f) & f
is_differentiable_on Z holds r(#)f is_differentiable_on Z & for x be Point of S
st x in Z holds ((r(#)f)`|Z)/.x =r*diff(f,x)
proof
let Z be Subset of S such that
A1: Z is open;
let r,f;
assume that
A2: Z c= dom (r(#)f) and
A3: f is_differentiable_on Z;
now
let x0 be Point of S;
assume x0 in Z;
then f is_differentiable_in x0 by A1,A3,Th31;
hence r(#)f is_differentiable_in x0 by Th37;
end;
hence
A4: r(#)f is_differentiable_on Z by A1,A2,Th31;
now
let x be Point of S;
assume
A5: x in Z;
then
A6: f is_differentiable_in x by A1,A3,Th31;
thus ((r(#)f)`|Z)/.x = diff((r(#)f),x) by A4,A5,Def9
.= r*diff(f,x) by A6,Th37;
end;
hence thesis;
end;
theorem
for Z be Subset of S st Z is open holds (Z c= dom f & f|Z is constant
implies f is_differentiable_on Z & for x be Point of S st x in Z holds (f`|Z)/.
x = 0.R_NormSpace_of_BoundedLinearOperators(S,T))
proof
let Z be Subset of S such that
A1: Z is open;
reconsider R = (the carrier of S) --> 0.T as PartFunc of S,T;
set L=0.R_NormSpace_of_BoundedLinearOperators(S,T);
assume that
A2: Z c= dom f and
A3: f|Z is constant;
R_NormSpace_of_BoundedLinearOperators(S,T) = NORMSTR (#
BoundedLinearOperators(S,T), Zero_(BoundedLinearOperators(S,T),
R_VectorSpace_of_LinearOperators(S,T)), Add_(BoundedLinearOperators(S,T),
R_VectorSpace_of_LinearOperators(S,T)), Mult_(BoundedLinearOperators(S,T),
R_VectorSpace_of_LinearOperators(S,T)), BoundedLinearOperatorsNorm(S,T) #) by
LOPBAN_1:def 14;
then reconsider L as Element of BoundedLinearOperators(S,T);
A4: dom R = the carrier of S;
now
let h;
assume h is non-zero;
A5: now
let n be Nat;
A6: R/.(h.n) =R.(h.n) by A4,PARTFUN1:def 6
.=0.T;
A7: rng h c= dom R;
A8: n in NAT by ORDINAL1:def 12;
thus ((||.h.||")(#)(R/*h)).n = (||.h.||".n)*((R/*h).n) by Def2
.=(||.h.||".n)*(R/.(h.n)) by A8,A7,FUNCT_2:109
.=0.T by A6,RLVECT_1:10;
end;
then
A9: (||.h.||")(#)(R/*h) is constant by VALUED_0:def 18;
hence (||.h.||")(#)(R/*h) is convergent by Th18;
((||.h.||")(#)(R/*h)).0 = 0.T by A5;
hence lim ((||.h.||")(#)(R/*h)) = 0.T by A9,Th18;
end;
then reconsider R as RestFunc of S,T by Def5;
consider r be Point of T such that
A10: for x be Point of S st x in Z/\dom f holds f.x=r by A3,PARTFUN2:57;
A11: now
let x be Point of S;
assume
A12: x in Z/\dom f;
Z/\ dom f c= dom f by XBOOLE_1:17;
hence f/.x=f.x by A12,PARTFUN1:def 6
.=r by A10,A12;
end;
A13: ((the carrier of S) --> 0.T) = L by LOPBAN_1:31;
A14: now
let x0 be Point of S;
assume
A15: x0 in Z;
then consider N being Neighbourhood of x0 such that
A16: N c= Z by A1,Th2;
A17: N c= dom f by A2,A16;
A18: x0 in Z/\dom f by A2,A15,XBOOLE_0:def 4;
for x be Point of S st x in N holds f/.x-f/.x0=L.(x-x0)+R/.(x-x0)
proof
let x be Point of S;
A19: R/.(x-x0) =R.(x-x0) by A4,PARTFUN1:def 6
.=0.T;
assume x in N;
then x in Z/\dom f by A16,A17,XBOOLE_0:def 4;
hence f/.x-f/.x0=r-f/.x0 by A11
.=r - r by A11,A18
.=0.T by RLVECT_1:15
.= 0.T + 0.T by RLVECT_1:4
.=L.(x-x0)+R/.(x-x0) by A13,A19;
end;
hence f is_differentiable_in x0 by A17;
end;
hence
A20: f is_differentiable_on Z by A1,A2,Th31;
let x0 be Point of S;
assume
A21: x0 in Z;
then consider N being Neighbourhood of x0 such that
A22: N c= Z by A1,Th2;
A23: N c= dom f by A2,A22;
A24: x0 in Z/\dom f by A2,A21,XBOOLE_0:def 4;
A25: for x be Point of S st x in N holds f/.x-f/.x0 =L.(x-x0)+R/.(x-x0)
proof
let x be Point of S;
A26: R/.(x-x0) =R.(x-x0) by A4,PARTFUN1:def 6
.=0.T;
assume x in N;
then x in Z/\dom f by A22,A23,XBOOLE_0:def 4;
hence f/.x - f/.x0 = r - f/.x0 by A11
.=r - r by A11,A24
.=0.T by RLVECT_1:15
.= 0.T + 0.T by RLVECT_1:4
.=L.(x-x0) + R/.(x-x0) by A13,A26;
end;
A27: f is_differentiable_in x0 by A14,A21;
thus (f`|Z)/.x0 = diff(f,x0) by A20,A21,Def9
.=0.R_NormSpace_of_BoundedLinearOperators(S,T) by A27,A23,A25,Def7;
end;
theorem
for f be PartFunc of S,S for r be Real for p be Point of S for Z be
Subset of S st Z is open holds ( Z c= dom f & (for x be Point of S st x in Z
holds f/.x = r*x + p) implies f is_differentiable_on Z & for x be Point of S st
x in Z holds (f`|Z)/.x = r * FuncUnit(S) )
proof
let f be PartFunc of S,S;
let r be Real;
let p be Point of S;
let Z be Subset of S such that
A1: Z is open;
A2: R_NormSpace_of_BoundedLinearOperators(S,S) = NORMSTR (#
BoundedLinearOperators(S,S), Zero_(BoundedLinearOperators(S,S),
R_VectorSpace_of_LinearOperators(S,S)), Add_(BoundedLinearOperators(S,S),
R_VectorSpace_of_LinearOperators(S,S)), Mult_(BoundedLinearOperators(S,S),
R_VectorSpace_of_LinearOperators(S,S)), BoundedLinearOperatorsNorm(S,S) #) by
LOPBAN_1:def 14;
then reconsider
II=FuncUnit(S) as Point of R_NormSpace_of_BoundedLinearOperators(
S,S);
set L = r * II;
reconsider L as Point of R_NormSpace_of_BoundedLinearOperators(S,S);
reconsider R = (the carrier of S) --> 0.S as PartFunc of S,S;
assume that
A3: Z c= dom f and
A4: for x be Point of S st x in Z holds f/.x = r*x + p;
A5: L=r*FuncUnit(S) by A2,LOPBAN_2:def 3;
A6: dom R = the carrier of S;
now
let h;
assume h is non-zero;
A7: now
let n be Nat;
A8: R/.(h.n) =R.(h.n) by A6,PARTFUN1:def 6
.=0.S;
A9: rng h c= dom R;
A10: n in NAT by ORDINAL1:def 12;
thus ((||.h.||")(#)(R/*h)).n = (||.h.||".n)*((R/*h).n) by Def2
.=(||.h.||".n)*(R/.(h.n)) by A10,A9,FUNCT_2:109
.=0.S by A8,RLVECT_1:10;
end;
then
A11: (||.h.||")(#)(R/*h) is constant by VALUED_0:def 18;
hence (||.h.||")(#)(R/*h) is convergent by Th18;
((||.h.||")(#)(R/*h)).0 = 0.S by A7;
hence lim ((||.h.||")(#)(R/*h)) = 0.S by A11,Th18;
end;
then reconsider R as RestFunc of S,S by Def5;
A12: now
let x0 be Point of S;
assume
A13: x0 in Z;
then consider N being Neighbourhood of x0 such that
A14: N c= Z by A1,Th2;
A15: for x be Point of S st x in N holds f/.x-f/.x0=L.(x-x0)+R/.(x-x0)
proof
let x be Point of S;
A16: R/.(x-x0) =R.(x-x0) by A6,PARTFUN1:def 6
.=0.S;
(x-x0)=(id the carrier of S).(x-x0);
then
A17: r* (x-x0)=r* ((FuncUnit(S)).(x-x0)) by LOPBAN_2:def 5
.=L.(x-x0) by LOPBAN_1:36;
assume x in N;
hence f/.x-f/.x0=r*x+p-f/.x0 by A4,A14
.=r*x+p - (r*x0+p) by A4,A13
.=r*x+(p-(r*x0+p)) by RLVECT_1:def 3
.=r*x+(p-r*x0-p) by RLVECT_1:27
.=r*x+(p+-r*x0-p)
.=r*x+(-r*x0+(p-p)) by RLVECT_1:def 3
.=r*x+(-r*x0+0.S) by RLVECT_1:15
.=r*x-r*x0 by RLVECT_1:4
.=r*(x-x0) by RLVECT_1:34
.=L.(x-x0)+R/.(x-x0) by A16,A17,RLVECT_1:4;
end;
N c= dom f by A3,A14;
hence f is_differentiable_in x0 by A15;
end;
hence
A18: f is_differentiable_on Z by A1,A3,Th31;
let x0 be Point of S;
assume
A19: x0 in Z;
then consider N being Neighbourhood of x0 such that
A20: N c= Z by A1,Th2;
A21: for x be Point of S st x in N holds f/.x-f/.x0=L.(x-x0)+R/.(x-x0)
proof
let x be Point of S;
A22: R/.(x-x0) =R.(x-x0) by A6,PARTFUN1:def 6
.=0.S;
(x-x0)=(id the carrier of S).(x-x0);
then
A23: r* (x-x0)=r* ((FuncUnit(S)).(x-x0)) by LOPBAN_2:def 5
.=L.(x-x0) by LOPBAN_1:36;
assume x in N;
hence f/.x - f/.x0 = r*x+p - f/.x0 by A4,A20
.=r*x+p-(r*x0+p) by A4,A19
.=r*x+(p-(r*x0+p)) by RLVECT_1:def 3
.=r*x+(p-r*x0-p) by RLVECT_1:27
.=r*x+(p+-r*x0-p)
.=r*x+(-r*x0+(p-p)) by RLVECT_1:def 3
.=r*x+(-r*x0+0.S) by RLVECT_1:15
.=r*x-r*x0 by RLVECT_1:4
.=r*(x-x0) by RLVECT_1:34
.=L.(x-x0)+R/.(x-x0) by A22,A23,RLVECT_1:4;
end;
A24: N c= dom f by A3,A20;
A25: f is_differentiable_in x0 by A12,A19;
thus (f`|Z)/.x0 = diff(f,x0) by A18,A19,Def9
.=r * FuncUnit(S) by A5,A25,A24,A21,Def7;
end;
theorem Th44:
for x0 be Point of S holds f is_differentiable_in x0 implies f
is_continuous_in x0
proof
let x0 be Point of S;
assume
A1: f is_differentiable_in x0;
then consider N being Neighbourhood of x0 such that
A2: N c= dom f and
ex L,R st for x be Point of S st x in N holds f/.x - f/.x0 = L.(x-x0 ) +
R/.(x-x0);
A3: now
consider g be Real such that
A4: 0<g and
A5: {y where y is Point of S:||.y-x0.|| < g } c= N by NFCONT_1:def 1;
reconsider s2 = NAT --> x0 as sequence of S;
let s1 be sequence of S such that
A6: rng s1 c= dom f and
A7: s1 is convergent and
A8: lim s1 = x0 and
A9: for n being Nat holds s1.n<>x0;
consider l be Nat such that
A10: for m be Nat st l<=m holds ||.s1.m-x0.||<g by A7,A8,A4,
NORMSP_1:def 7;
deffunc G(Nat) = s1.$1-s2.$1;
consider s3 be sequence of S such that
A11: for n holds s3.n=G(n) from FUNCT_2:sch 4;
A12: for n being Nat holds s3.n=G(n)
proof let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A11;
end;
A13: now
given n such that
A14: s3.n=0.S;
s1.n-s2.n=0.S by A12,A14;
then s1.n-x0=0.S;
hence contradiction by A9,RLVECT_1:21;
end;
now
given n being Nat such that
A15: (s3^\l).n=0.S;
A16: n+l in NAT by ORDINAL1:def 12;
s3.(n+l)=0.S by A15,NAT_1:def 3;
hence contradiction by A13,A16;
end;
then
A17: s3^\l is non-zero by Th7;
reconsider c =s2^\l as constant sequence of S;
A18: s3=s1-s2 by A12,NORMSP_1:def 3;
A19: s2 is convergent by Th18;
then
A20: s3 is convergent by A7,A18,NORMSP_1:20;
then
A21: s3^\l is convergent by LOPBAN_3:9;
lim s2 = s2.0 by Th18
.=x0;
then lim s3 =x0-x0 by A7,A8,A19,A18,NORMSP_1:26
.=0.S by RLVECT_1:15;
then lim(s3^\l)=0.S by A20,LOPBAN_3:9;
then reconsider h=s3^\l as (0.S)-convergent sequence of S
by A21,Def4;
now
let n;
thus (f/*(h+c)-f/*c+f/*c).n =(f/*(h+c)-f/*c).n+(f/*c).n by NORMSP_1:def 2
.=(f/*(h+c)).n-(f/*c).n+(f/*c).n by NORMSP_1:def 3
.=(f/*(h+c)).n-((f/*c).n-(f/*c).n) by RLVECT_1:29
.=(f/*(h+c)).n-0.T by RLVECT_1:15
.=(f/*(h+c)).n by RLVECT_1:13;
end;
then
A22: f/*(h+c)-f/*c+(f/*c)=f/*(h+c) by FUNCT_2:63;
now
let n;
thus (h+c).n=((s1-s2+s2)^\l).n by A18,Th15
.=(s1-s2+s2).(n+l) by NAT_1:def 3
.=(s1-s2).(n+l)+s2.(n+l) by NORMSP_1:def 2
.=s1.(n+l)-s2.(n+l)+s2.(n+l) by NORMSP_1:def 3
.=s1.(n+l)-(s2.(n+l)-s2.(n+l)) by RLVECT_1:29
.=s1.(n+l)-0.S by RLVECT_1:15
.=s1.(l+n) by RLVECT_1:13
.=(s1^\l).n by NAT_1:def 3;
end;
then
A23: f/*(h+c)-f/*c+(f/*c)=f/*(s1^\l) by A22,FUNCT_2:63
.=(f/*s1)^\l by A6,VALUED_0:27;
A24: rng c = {x0}
proof
thus rng c c= {x0}
proof
let y be object;
assume y in rng c;
then consider n being Nat such that
A25: y=(s2^\l).n by NFCONT_1:6;
A26: n+l in NAT by ORDINAL1:def 12;
y=s2.(n+l) by A25,NAT_1:def 3;
then y=x0 by FUNCOP_1:7,A26;
hence thesis by TARSKI:def 1;
end;
let y be object;
assume y in {x0};
then
A27: y=x0 by TARSKI:def 1;
A28: 0+l in NAT by ORDINAL1:def 12;
c.0=s2.(0+l) by NAT_1:def 3
.= y by A27,FUNCOP_1:7,A28;
hence thesis by NFCONT_1:6;
end;
A29: now
let p be Real such that
A30: 0<p;
reconsider n=0 as Nat;
take n;
let m be Nat such that
n<=m;
A31: m in NAT by ORDINAL1:def 12;
A32: m+l in NAT by ORDINAL1:def 12;
x0 in N by NFCONT_1:4;
then rng c c= dom f by A2,A24,ZFMISC_1:31;
then ||.(f/*c).m-f/.x0.|| =||.f/.(c.m)-f/.x0.|| by FUNCT_2:109,A31
.=||.f/.(s2.(m+l))-f/.x0.|| by NAT_1:def 3
.=||.f/.x0-f/.x0.|| by FUNCOP_1:7,A32
.=||.0.T.|| by RLVECT_1:15
.=0 by NORMSP_1:1;
hence ||.(f/*c).m-f/.x0.||<p by A30;
end;
then
A33: f/*c is convergent;
A34: rng (h+c) c= N
proof
let y be object;
assume
A35: y in rng(h+c);
then consider n being Nat such that
A36: y=(h+c).n by NFCONT_1:6;
reconsider y1=y as Point of S by A35;
(h+c).n=((s1-s2+s2)^\l).n by A18,Th15
.=(s1-s2+s2).(n+l) by NAT_1:def 3
.=(s1-s2).(n+l)+s2.(n+l) by NORMSP_1:def 2
.=s1.(n+l)-s2.(n+l)+s2.(n+l) by NORMSP_1:def 3
.=s1.(n+l)-(s2.(n+l)-s2.(n+l)) by RLVECT_1:29
.=s1.(n+l)-0.S by RLVECT_1:15
.=s1.(l+n) by RLVECT_1:13;
then ||.(h+c).n-x0.||<g by A10,NAT_1:12;
then y1 in {z where z is Point of S:||.z-x0.|| < g } by A36;
hence thesis by A5;
end;
then
A37: (f/*(h+c) - f/*c) is convergent by A17,A1,A2,A24,Th34;
then f/*(h+c)-f/*c+f/*c is convergent by A33,NORMSP_1:19;
hence f/*s1 is convergent by A23,LOPBAN_3:10;
A38: lim (f/*(h+c) - f/*c) = 0.T by A17,A1,A2,A24,A34,Th34;
lim(f/*c)=f/.x0 by A29,A33,NORMSP_1:def 7;
then lim(f/*(h+c)-f/*c+f/*c)=0.T +f/.x0 by A37,A38,A33,NORMSP_1:25
.=f/.x0 by RLVECT_1:4;
hence f/.x0=lim(f/*s1) by A37,A33,A23,LOPBAN_3:11,NORMSP_1:19;
end;
x0 in N by NFCONT_1:4;
hence thesis by A2,A3,Th27;
end;
theorem
f is_differentiable_on X implies f is_continuous_on X
by Th44;
theorem
for Z be Subset of S st Z is open holds ( f is_differentiable_on X & Z
c= X implies f is_differentiable_on Z )
proof
let Z be Subset of S such that
A1: Z is open;
assume that
A2: f is_differentiable_on X and
A3: Z c= X;
X c= dom f by A2;
hence
A4: Z c= dom f by A3;
let x0;
assume
A5: x0 in Z;
then consider N1 being Neighbourhood of x0 such that
A6: N1 c= Z by A1,Th2;
f|X is_differentiable_in x0 by A2,A3,A5;
then consider N being Neighbourhood of x0 such that
A7: N c= dom(f|X) and
A8: ex L,R st for x be Point of S st x in N holds (f|X)/.x-(f|X)/.x0=L.(
x-x0)+R/.(x-x0);
consider N2 being Neighbourhood of x0 such that
A9: N2 c= N and
A10: N2 c= N1 by Th1;
A11: N2 c= Z by A6,A10;
take N2;
dom(f|X)=dom f/\X by RELAT_1:61;
then dom(f|X) c=dom f by XBOOLE_1:17;
then N c= dom f by A7;
then N2 c=dom f by A9;
then N2 c=dom f/\Z by A11,XBOOLE_1:19;
hence
A12: N2 c=dom(f|Z) by RELAT_1:61;
consider L,R such that
A13: for x be Point of S st x in N holds (f|X)/.x-(f|X)/.x0=L.(x-x0)+R/.
(x-x0) by A8;
take L,R;
let x be Point of S;
assume
A14: x in N2;
then (f|X)/.x-(f|X)/.x0=L.(x-x0)+R/.(x-x0) by A9,A13;
then
A15: (f|X)/.x-f/.x0=L.(x-x0)+R/.(x-x0) by A3,A4,A5,PARTFUN2:17;
x in N by A9,A14;
then f/.x-f/.x0=L.(x-x0)+R/.(x-x0) by A7,A15,PARTFUN2:15;
then f/.x-(f|Z)/.x0=L.(x-x0)+R/.(x-x0) by A4,A5,PARTFUN2:17;
hence thesis by A12,A14,PARTFUN2:15;
end;
theorem
f is_differentiable_in x0 implies ex N being Neighbourhood of x0 st N
c= dom f & ex R st R/.0.S=0.T & R is_continuous_in 0.S & for x be Point of S st
x in N holds f/.x-f/.x0 = diff(f,x0).(x-x0) + R/.(x-x0)
proof
assume f is_differentiable_in x0;
then consider N being Neighbourhood of x0 such that
A1: N c= dom f and
A2: ex R st for x be Point of S st x in N holds f/.x - f/.x0 = diff(f,x0
).(x-x0) + R/.(x-x0) by Def7;
take N;
ex R st R/.0.S=0.T & R is_continuous_in 0.S & for x be Point of S st x
in N holds f/.x-f/.x0 = diff(f,x0).(x-x0) + R/.(x-x0)
proof
R_NormSpace_of_BoundedLinearOperators(S,T) = NORMSTR (#
BoundedLinearOperators(S,T), Zero_(BoundedLinearOperators(S,T),
R_VectorSpace_of_LinearOperators(S,T)), Add_(BoundedLinearOperators(S,T),
R_VectorSpace_of_LinearOperators(S,T)), Mult_(BoundedLinearOperators(S,T),
R_VectorSpace_of_LinearOperators(S,T)), BoundedLinearOperatorsNorm(S,T) #) by
LOPBAN_1:def 14;
then reconsider L =diff(f,x0) as Element of BoundedLinearOperators(S,T);
consider R such that
A3: for x be Point of S st x in N holds f/.x-f/.x0 = diff(f,x0).(x-x0)
+ R/.(x-x0) by A2;
take R;
f/.x0 - f/.x0 = L.(x0-x0) + R/.(x0-x0) by A3,NFCONT_1:4;
then 0.T = L.(x0-x0) + R/.(x0-x0) by RLVECT_1:15;
then 0.T = L.0.S + R/.(x0-x0) by RLVECT_1:15;
then
A4: 0.T = L.0.S + R/.0.S by RLVECT_1:15;
L.(0.S) =modetrans(L,S,T).(0.S) by LOPBAN_1:def 11
.= modetrans(L,S,T).(0*0.S) by RLVECT_1:10
.=0*modetrans(L,S,T).0.S by LOPBAN_1:def 5
.=0.T by RLVECT_1:10;
hence
A5: R/.0.S=0.T by A4,RLVECT_1:4;
A6: now
let s1 be sequence of S;
assume that
rng s1 c= dom R and
A7: s1 is convergent & lim s1 = 0.S and
A8: for n being Nat holds s1.n<>0.S;
A9: s1 is (0.S)-convergent sequence of S by A7,Def4;
s1 is non-zero by A8,Th7;
hence R/*s1 is convergent & lim (R/*s1)=R/.(0.S) by A5,A9,Th24;
end;
R is total by Def5;
then dom R=the carrier of S by PARTFUN1:def 2;
hence thesis by A3,A6,Th27;
end;
hence thesis by A1;
end;
definition
let S be non trivial RealNormSpace ,T;
let IT be PartFunc of S,T;
redefine attr IT is RestFunc-like means :: redefines RestFunc-like (NDIFF_1, definition)
IT is total & for h be
non-zero (0.S)-convergent sequence of S
holds (||.h.||")(#)(IT /*h) is convergent
& lim ((||.h.||")(#)(IT/*h)) = 0.T;
correctness;
end;