Copyright (c) 1990 Association of Mizar Users
environ
vocabulary RLVECT_1, BINOP_1, FUNCT_1, PRE_TOPC, RLSUB_1, ABSVALUE, ARYTM_1,
ARYTM_3, RELAT_1, SEQM_3, SEQ_2, SEQ_1, ORDINAL2, NORMSP_1, ARYTM;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0,
REAL_1, NAT_1, FUNCT_1, FUNCT_2, BINOP_1, RELAT_1, SEQ_1, SEQ_2, SEQM_3,
ABSVALUE, STRUCT_0, PRE_TOPC, RLVECT_1, RLSUB_1;
constructors REAL_1, NAT_1, DOMAIN_1, SEQ_2, SEQM_3, ABSVALUE, RLSUB_1,
MEMBERED, XBOOLE_0;
clusters STRUCT_0, XREAL_0, RELSET_1, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0,
NUMBERS, ORDINAL2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions RLVECT_1, SEQM_3, STRUCT_0;
theorems TARSKI, AXIOMS, REAL_1, NAT_1, FUNCT_1, SQUARE_1, SEQ_2, ABSVALUE,
RLVECT_1, RLSUB_1, FUNCT_2, SEQM_3, STRUCT_0, RELSET_1, XREAL_0,
XBOOLE_0, XCMPLX_0, XCMPLX_1;
schemes FUNCT_1, FUNCT_2, SEQ_1, NAT_1;
begin
definition
struct(RLSStruct) NORMSTR (# carrier -> set,
Zero -> Element of the carrier,
add -> BinOp of the carrier,
Mult -> Function of [:REAL, the carrier:], the carrier,
norm -> Function of the carrier, REAL #);
end;
definition
cluster non empty NORMSTR;
existence
proof
consider A being non empty set, Z being Element of A,
a being BinOp of A, M being Function of [:REAL,A:],A,
n being Function of A,REAL;
take NORMSTR(#A,Z,a,M,n#);
thus the carrier of NORMSTR(#A,Z,a,M,n#) is non empty;
end;
end;
reserve X for non empty NORMSTR;
reserve a, b for Real;
reserve x for Point of X;
deffunc 0'(NORMSTR) = 0.$1;
definition let X, x;
func ||.x.|| -> Real equals
:Def1: ( the norm of X ).x;
coherence;
end;
consider V being RealLinearSpace;
Lm1: the carrier of (0).V = {0.V} by RLSUB_1:def 3;
deffunc F(set) = 0;
consider nil_to_nil being Function
of the carrier of (0).V , REAL such that
Lm2: for u being VECTOR of (0).V holds nil_to_nil.u = F(u) from LambdaD;
Lm3:
nil_to_nil.(0.V) = 0
proof
0.V is VECTOR of (0).V by Lm1,TARSKI:def 1;
hence thesis by Lm2;
end;
Lm4:
for u being VECTOR of (0).V , a holds
nil_to_nil.(a * u) = abs(a) * nil_to_nil.u
proof
let u be VECTOR of (0).V;
let a;
nil_to_nil.u = 0 by Lm1,Lm3,TARSKI:def 1;
hence thesis by Lm1,Lm3,TARSKI:def 1;
end;
Lm5:
for u , v being VECTOR of (0).V holds
nil_to_nil.(u + v) <= nil_to_nil.u + nil_to_nil.v
proof
let u, v be VECTOR of (0).V;
u = 0.V & v = 0.V by Lm1,TARSKI:def 1;
hence thesis by Lm1,Lm3,TARSKI:def 1;
end;
reconsider X =
NORMSTR (# the carrier of (0).V, the Zero of (0).V, the add of (0).V,
the Mult of (0).V, nil_to_nil #)
as non empty NORMSTR by STRUCT_0:def 1;
Lm6:
now
let x, y be Point of X;
let a;
A1: ||.x.|| = nil_to_nil.x &
||.y.|| = nil_to_nil.y &
||.a * x.|| = nil_to_nil.(a * x) &
||.x + y.|| = nil_to_nil.(x + y) by Def1;
reconsider u = x, w = y as VECTOR of (0).V;
thus ||.x.|| = 0 iff x = 0'(X)
proof
0'(X) = the Zero of X by RLVECT_1:def 2
.= 0.(0).V by RLVECT_1:def 2
.= 0.V by RLSUB_1:19;
hence thesis by Def1,Lm1,Lm3,TARSKI:def 1;
end;
a * x = (the Mult of X).[a,u] by RLVECT_1:def 4
.= a * u by RLVECT_1:def 4;
hence ||.a * x.|| = abs(a) * ||.x.|| by A1,Lm4;
x + y = (the add of X).[x,y] by RLVECT_1:def 3
.= u + w by RLVECT_1:def 3;
hence ||.x + y.|| <= ||.x.|| + ||.y.|| by A1,Lm5;
end;
definition let IT be non empty NORMSTR;
attr IT is RealNormSpace-like means
:Def2: for x , y being Point of IT , a holds
( ||.x.|| = 0 iff x = 0.IT ) &
||.a * x.|| = abs(a) * ||.x.|| &
||.x + y.|| <= ||.x.|| + ||.y.||;
end;
definition
cluster RealNormSpace-like RealLinearSpace-like Abelian
add-associative right_zeroed right_complementable strict
(non empty NORMSTR);
existence
proof
take X;
thus X is RealNormSpace-like by Def2,Lm6;
A1: now
let x,y be VECTOR of X;
let x',y' be VECTOR of (0).V;
assume A2: x = x' & y = y';
hence x + y= (the add of X).[x',y'] by RLVECT_1:def 3 .=
x' + y' by RLVECT_1:def 3;
let a;
thus a * x = (the Mult of X).[a,x'] by A2,RLVECT_1:def 4 .=
a * x' by RLVECT_1:def 4;
end;
A3: 0.X = the Zero of X by RLVECT_1:def 2 .=
0.(0).V by RLVECT_1:def 2;
thus X is RealLinearSpace-like
proof
thus for a for v,w being VECTOR of X holds a * (v + w) = a * v + a * w
proof
let a;
let v,w be VECTOR of X;
reconsider v'= v, w' = w as VECTOR of (0).V;
A4: a * v' = a * v by A1;
A5: a * w' = a * w by A1;
v + w = v'+ w' by A1;
hence a * (v + w) = a *( v' + w') by A1 .=
a * v' + a * w' by RLVECT_1:def 9 .= a * v + a * w by A1,A4,A5;
end;
thus for a,b for v being VECTOR of X holds (a + b) * v = a * v + b * v
proof
let a,b;
let v be VECTOR of X;
reconsider v'= v as VECTOR of (0).V;
A6: a * v' = a * v by A1;
A7: b * v' = b * v by A1;
thus (a + b) * v = (a + b) * v' by A1 .=
a * v' + b * v' by RLVECT_1:def 9 .= a * v + b * v by A1,A6,A7;
end;
thus for a,b for v being VECTOR of X holds (a * b) * v = a * (b * v)
proof
let a,b;
let v be VECTOR of X;
reconsider v'= v as VECTOR of (0).V;
A8: b * v' = b * v by A1;
thus (a * b) * v = (a * b) * v' by A1
.= a * (b * v') by RLVECT_1:def 9
.= a * (b * v) by A1,A8;
end;
let v be VECTOR of X;
reconsider v'= v as VECTOR of (0).V;
thus 1 * v = 1 * v' by A1 .= v by RLVECT_1:def 9;
end;
thus for v,w being VECTOR of X holds v + w = w + v
proof
let v,w be VECTOR of X;
reconsider v'= v , w'= w as VECTOR of (0).V;
thus v + w = w'+ v' by A1 .= w + v by A1;
end;
thus for u,v,w being VECTOR of X holds (u + v) + w = u + (v + w)
proof
let u,v,w be VECTOR of X;
reconsider u'= u, v'= v, w'= w as VECTOR of (0).V;
A9: u + v = u'+ v' by A1;
A10: v + w = v' + w' by A1;
thus (u + v) + w = (u' + v') + w' by A1,A9 .=
u' + (v' + w') by RLVECT_1:def 6 .= u + (v + w) by A1,A10;
end;
thus for v being VECTOR of X holds v + 0.X = v
proof
let v be VECTOR of X;
reconsider v'= v as VECTOR of (0).V;
thus v + 0.X = v'+ 0.(0).V by A1,A3 .=v by RLVECT_1:10;
end;
thus for v being VECTOR of X
ex w being VECTOR of X st v + w = 0.X
proof
let v be VECTOR of X;
reconsider v'= v as VECTOR of (0).V;
consider w' be VECTOR of (0).V such that
A11: v' + w' = 0.(0).V by RLVECT_1:def 8;
reconsider w = w' as VECTOR of X;
take w;
thus v + w = 0.X by A1,A3,A11;
end;
thus thesis;
end;
end;
definition
mode RealNormSpace is RealNormSpace-like RealLinearSpace-like
Abelian add-associative right_zeroed right_complementable
(non empty NORMSTR);
end;
reserve RNS for RealNormSpace;
reserve x, y, z, g, g1, g2 for Point of RNS;
canceled 4;
theorem
||.0.RNS.|| = 0 by Def2;
theorem Th6:
||.-x.|| = ||.x.||
proof
A1: ||.-x.|| = ||.(-1) * x.|| by RLVECT_1:29
.= abs(-1 ) * ||.x.|| by Def2;
abs(-1 ) = -(-1) by ABSVALUE:def 1
.= 1;
hence thesis by A1;
end;
theorem Th7:
||.x - y.|| <= ||.x.|| + ||.y.||
proof
x - y = x + (-y) by RLVECT_1:def 11;
then ||.x - y.|| <= ||.x.|| + ||.(-y).|| by Def2;
hence thesis by Th6;
end;
theorem Th8:
0 <= ||.x.||
proof
||.x - x.|| = ||.0'(RNS).|| by RLVECT_1:28
.= 0 by Def2;
then 0 <= ||.x.|| + ||.x.|| by Th7;
then 0 <= (||.x.|| + ||.x.||)/2 by SQUARE_1:27;
hence thesis by XCMPLX_1:65;
end;
theorem
||.a * x + b * y.|| <= abs(a) * ||.x.|| + abs(b) * ||.y.||
proof
||.a * x + b * y.|| <= ||.a * x.|| + ||.b * y.|| by Def2;
then ||.a * x + b * y.|| <= abs(a) * ||.x.|| + ||.b * y.|| by Def2;
hence thesis by Def2;
end;
theorem Th10:
||.x - y.|| = 0 iff x = y
proof
||.x - y.|| = 0 iff x - y = 0'(RNS) by Def2;
hence thesis by RLVECT_1:28,35;
end;
theorem Th11:
||.x - y.|| = ||.y - x.||
proof
x - y = (-y) + x by RLVECT_1:def 11
.= - (y - x) by RLVECT_1:47;
hence thesis by Th6;
end;
theorem Th12:
||.x.|| - ||.y.|| <= ||.x - y.||
proof
(x - y) + y = x - (y - y) by RLVECT_1:43
.= x - 0'(RNS) by RLVECT_1:28
.= x by RLVECT_1:26;
then ||.x.|| <= ||.x - y.|| + ||.y.|| by Def2;
hence thesis by REAL_1:86;
end;
theorem Th13:
abs(||.x.|| - ||.y.||) <= ||.x - y.||
proof
A1: ||.x.|| - ||.y.|| <= ||.x - y.|| by Th12;
(y - x) + x = y - (x - x) by RLVECT_1:43
.= y - 0'(RNS) by RLVECT_1:28
.= y by RLVECT_1:26;
then ||.y.|| <= ||.y - x.|| + ||.x.|| by Def2;
then ||.y.|| - ||.x.|| <= ||.y - x.|| by REAL_1:86;
then ||.y.|| - ||.x.|| <= ||.x - y.|| by Th11;
then -(||.x.|| - ||.y.||) <= ||.x - y.|| by XCMPLX_1:143;
then -||.x - y.|| <= -(-(||.x.|| - ||.y.||)) by REAL_1:50;
hence thesis by A1,ABSVALUE:12;
end;
theorem Th14:
||.x - z.|| <= ||.x - y.|| + ||.y - z.||
proof
x - z = x + (-z) by RLVECT_1:def 11
.= x + (0'(RNS) + (-z)) by RLVECT_1:10
.= x + (((-y) + y) + (-z)) by RLVECT_1:16
.= x + ((-y) + (y + (-z))) by RLVECT_1:def 6
.= (x + (-y)) + (y + (-z)) by RLVECT_1:def 6
.= (x - y) + (y + (-z)) by RLVECT_1:def 11
.= (x - y) + (y - z) by RLVECT_1:def 11;
hence thesis by Def2;
end;
theorem
x <> y implies ||.x - y.|| <> 0 by Th10;
definition let RNS be 1-sorted;
mode sequence of RNS means
:Def3: it is Function of NAT, the carrier of RNS;
existence
proof consider f being Function of NAT, the carrier of RNS;
take f;
thus thesis;
end;
end;
definition let RNS be 1-sorted;
cluster -> Function-like Relation-like sequence of RNS;
coherence by Def3;
end;
definition let RNS be non empty 1-sorted;
redefine mode sequence of RNS -> Function of NAT, the carrier of RNS;
coherence by Def3;
end;
reserve S, S1, S2 for sequence of RNS;
reserve k, n, m, m1, m2 for Nat;
reserve r for Real;
reserve f for Function;
reserve d, s, t for set;
canceled;
theorem Th17:
for RNS being non empty 1-sorted, x being Element of RNS
holds f is sequence of RNS iff ( dom f = NAT &
for d st d in NAT holds f.d is Element of RNS )
proof
let RNS be non empty 1-sorted;
let x be Element of RNS;
thus f is sequence of RNS implies
( dom f = NAT & for d st d in NAT holds f.d
is Element of RNS )
proof
assume
A1: f is sequence of RNS;
then A2: dom f = NAT by FUNCT_2:def 1;
A3: rng f c= the carrier of RNS by A1,RELSET_1:12;
for d st d in NAT holds f.d is Element of RNS
proof
let d; assume
d in NAT;
then f.d in rng f by A2,FUNCT_1:def 5;
hence thesis by A3;
end;
hence thesis by A1,FUNCT_2:def 1;
end;
thus ( dom f = NAT & for d st d in NAT holds f.d
is Element of RNS )
implies f is sequence of RNS
proof
assume that
A4: dom f = NAT and
A5: for d st d in NAT holds f.d is Element of RNS;
for s st s in rng f holds
s in the carrier of RNS
proof
let s; assume
s in rng f;
then consider d such that
A6: d in dom f and
A7: s = f.d by FUNCT_1:def 5;
f.d is Element of RNS by A4,A5,A6;
hence thesis by A7;
end;
then rng f c= the carrier of RNS by TARSKI:def 3;
then f is Function of NAT, the carrier of RNS by A4,FUNCT_2:def 1,
RELSET_1:11;
hence thesis by Def3;
end;
end;
canceled;
theorem Th19:
for RNS being non empty 1-sorted, x being Element of RNS
ex S being sequence of RNS st rng S = {x}
proof
let RNS be non empty 1-sorted;
let x be Element of RNS;
consider f such that
A1: dom f = NAT and
A2: rng f = {x} by FUNCT_1:15;
f is Function of NAT, the carrier of RNS by A1,A2,FUNCT_2:def 1,RELSET_1:
11
;
then reconsider f as sequence of RNS by Def3;
take f;
thus thesis by A2;
end;
theorem Th20:
for RNS being non empty 1-sorted, S being sequence of RNS st
(ex x being Element of RNS st for n holds S.n = x)
ex x being Element of RNS st rng S={x}
proof
let RNS be non empty 1-sorted;
let S be sequence of RNS;
given z being Element of RNS such that
A1: for n holds S.n = z;
take x = z;
now let t; assume t in rng S;
then consider d such that
A2: d in dom S and
A3: S.d = t by FUNCT_1:def 5;
d in NAT by A2,FUNCT_2:def 1;
then t = z by A1,A3;
hence t in {x} by TARSKI:def 1;
end;
then A4: rng S c= {x} by TARSKI:def 3;
now let s; assume
s in {x};
then A5: s = x by TARSKI:def 1;
now assume
A6: not s in rng S;
now let n;
n in NAT;
then n in dom S by FUNCT_2:def 1;
then S.n <> x by A5,A6,FUNCT_1:def 5;
hence contradiction by A1;
end;
hence contradiction;
end;
hence s in rng S;
end;
then {x} c= rng S by TARSKI:def 3;
hence thesis by A4,XBOOLE_0:def 10;
end;
theorem Th21:
for RNS being non empty 1-sorted, S being sequence of RNS st
ex x being Element of RNS
st rng S = {x} holds for n holds S.n = S.(n+1)
proof
let RNS be non empty 1-sorted;
let S be sequence of RNS;
given z being Element of RNS such that
A1: rng S = {z};
let n;
n in NAT & (n+1) in NAT;
then n in dom S & (n+1) in dom S by FUNCT_2:def 1;
then S.n in {z} & S.(n+1) in {z} by A1,FUNCT_1:def 5;
then S.n = z & S.(n+1) = z by TARSKI:def 1;
hence thesis;
end;
theorem Th22:
for RNS being non empty 1-sorted, S being sequence of RNS st
for n holds S.n = S.(n+1)
holds for n , k holds S.n = S.(n+k)
proof
let RNS be non empty 1-sorted;
let S be sequence of RNS;
assume
A1: for n holds S.n = S.(n+1);
let n;
defpred P[Nat] means S.n = S.(n+$1);
A2: P[0];
A3: now let k such that
A4: P[k];
S.(n+k) = S.(n+k+1) by A1;
hence P[k+1] by A4,XCMPLX_1:1;
end;
thus for k holds P[k] from Ind(A2,A3);
end;
theorem Th23:
for RNS being non empty 1-sorted, S being sequence of RNS st
for n , k holds S.n = S.(n+k)
holds for n , m holds S.n = S.m
proof
let RNS be non empty 1-sorted;
let S be sequence of RNS;
assume
A1: for n , k holds S.n = S.(n+k);
let n , m;
A2: now assume n <= m;
then ex k st m = n + k by NAT_1:28;
hence S.n = S.m by A1;
end;
now assume m <= n;
then ex k st n = m + k by NAT_1:28;
hence S.n = S.m by A1;
end;
hence thesis by A2;
end;
theorem Th24:
for RNS being non empty 1-sorted, S being sequence of RNS st
for n , m holds S.n = S.m
ex x being Element of RNS st for n holds S.n = x
proof
let RNS be non empty 1-sorted;
let S be sequence of RNS;
assume that
A1: for n , m holds S.n = S.m and
A2: for x being Element of RNS ex n st S.n <> x;
now let n;
consider z being Element of RNS such that
A3: S.n = z;
ex k st S.k <> z by A2;
hence contradiction by A1,A3;
end;
hence thesis;
end;
theorem
ex S st rng S = {0.RNS} by Th19;
definition let RNS be non empty 1-sorted;
let S be sequence of RNS;
redefine attr S is constant means :Def4:
ex x being Element of RNS st for n holds S.n = x;
compatibility
proof
A1: dom S = NAT by FUNCT_2:def 1;
hereby assume
A2: S is constant;
consider n0 being Nat;
take r = S.n0;
let n be Nat;
thus S.n = r by A1,A2,SEQM_3:def 5;
end;
given r being Element of RNS such that
A3: for n holds S.n=r;
let n1,n2 be set;
assume
A4: n1 in dom S & n2 in dom S;
hence S.n1 = r by A1,A3 .= S.n2 by A1,A3,A4;
end;
end;
canceled;
theorem
for RNS being non empty 1-sorted, S being sequence of RNS holds
S is constant iff ex x being Element of RNS st rng S = {x}
proof
let RNS be non empty 1-sorted;
let S be sequence of RNS;
thus S is constant implies
ex x being Element of RNS st rng S = {x}
proof
assume
S is constant;
then ex x being Element of RNS st for n holds S.n = x
by Def4;
hence thesis by Th20;
end;
assume ex x being Element of RNS st rng S = {x};
then ( for n holds S.n = S.(n+1) ) by Th21;
then ( for n , k holds S.n = S.(n+k) ) by Th22;
then ( for n , m holds S.n = S.m ) by Th23;
then ( ex x being Element of RNS st for n holds S.n =
x )
by Th24;
hence thesis by Def4;
end;
Lm7:
for RNS being non empty 1-sorted
for S being sequence of RNS
for n holds S.n is Element of RNS;
definition let RNS be non empty 1-sorted;
let S be sequence of RNS;
let n;
redefine func S.n -> Element of RNS;
coherence by Lm7;
end;
scheme ExRNSSeq{RNS()->RealNormSpace, F(Nat) -> ( Point of RNS() ) } :
ex S be sequence of RNS() st for n holds S.n = F(n)
proof
defpred P[set,set] means ex n st n =$1 & $2 = F(n);
A1: for d st d in NAT ex s st P[d,s]
proof
let d; assume d in NAT;
then consider n such that
A2: n = d;
reconsider z = F(n) as set;
take z;
thus thesis by A2;
end;
A3: for d , s , t st d in NAT & P[d,s] & P[d,t] holds s = t;
consider f such that
A4: dom f = NAT and
A5: for d st d in NAT holds P[d,f.d] from FuncEx(A3,A1);
for d st d in NAT holds f.d is Point of RNS()
proof
let d; assume d in NAT;
then ex n st n = d & f.d = F(n) by A5;
hence thesis;
end;
then reconsider f as sequence of RNS() by A4,Th17;
take S = f;
now let n;
P[n,S.n] by A5;
hence S.n = F(n);
end;
hence for n holds S.n = F(n);
end;
scheme ExRLSSeq{RNS()->RealLinearSpace,
F(Nat) -> Element of RNS() } :
ex S be sequence of RNS() st for n holds S.n = F(n)
proof
defpred P[set,set] means ex n st ( n =$1 & $2 = F(n));
A1: for d st d in NAT ex s st P[d,s]
proof
let d; assume d in NAT;
then consider n such that
A2: n = d;
reconsider z = F(n) as set;
take z;
thus thesis by A2;
end;
A3: for d , s , t st d in NAT & P[d,s] & P[d,t] holds s = t;
consider f such that
A4: dom f = NAT and
A5: for d st d in NAT holds P[d,f.d] from FuncEx(A3,A1);
for d st d in NAT holds f.d is Element of RNS()
proof
let d; assume d in NAT;
then ex n st n = d & f.d = F(n) by A5;
hence thesis;
end;
then reconsider f as sequence of RNS() by A4,Th17;
take S = f;
now let n;
P[n,S.n] by A5;
hence S.n = F(n);
end;
hence for n holds S.n = F(n);
end;
definition let RNS be RealLinearSpace;
let S1, S2 be sequence of RNS;
func S1 + S2 -> sequence of RNS means
:Def5: for n holds it.n = S1.n + S2.n;
existence proof
deffunc F(Nat) = S1.$1 + S2.$1;
thus ex S being sequence of RNS st for n holds S.n = F(n) from ExRLSSeq;
end;
uniqueness
proof
let S, T be sequence of RNS;
assume that
A1: ( for n holds S.n = S1.n + S2.n ) and
A2: ( for n holds T.n = S1.n + S2.n );
for n holds S.n = T.n
proof
let n;
S.n = S1.n + S2.n by A1;
hence thesis by A2;
end;
hence thesis by FUNCT_2:113;
end;
end;
definition let RNS be RealLinearSpace;
let S1 , S2 be sequence of RNS;
func S1 - S2 -> sequence of RNS means
:Def6: for n holds it.n = S1.n - S2.n;
existence proof
deffunc F(Nat) = S1.$1 - S2.$1;
thus ex S being sequence of RNS st for n holds S.n = F(n) from ExRLSSeq;
end;
uniqueness
proof
let S , T be sequence of RNS;
assume that
A1: ( for n holds S.n = S1.n - S2.n ) and
A2: ( for n holds T.n = S1.n - S2.n );
for n holds S.n = T.n
proof
let n;
S.n = S1.n - S2.n by A1;
hence thesis by A2;
end;
hence thesis by FUNCT_2:113;
end;
end;
definition let RNS be RealLinearSpace;
let S be sequence of RNS;
let x be Element of RNS;
func S - x -> sequence of RNS means
:Def7: for n holds it.n = S.n - x;
existence proof
deffunc F(Nat) = S.$1 - x;
thus ex S being sequence of RNS st for n holds S.n = F(n) from ExRLSSeq;
end;
uniqueness
proof
let S1 , S2 be sequence of RNS;
assume that
A1: ( for n holds S1.n = S.n - x ) and
A2: ( for n holds S2.n = S.n - x );
for n holds S1.n = S2.n
proof
let n;
S1.n = S.n - x by A1;
hence thesis by A2;
end;
hence thesis by FUNCT_2:113;
end;
end;
definition let RNS be RealLinearSpace;
let S be sequence of RNS;
let a;
func a * S -> sequence of RNS means
:Def8: for n holds it.n = a * S.n;
existence proof
deffunc F(Nat) = a * S.$1;
thus ex S being sequence of RNS st for n holds S.n = F(n) from ExRLSSeq;
end;
uniqueness
proof
let S1 , S2 be sequence of RNS;
assume that
A1: ( for n holds S1.n = a * S.n ) and
A2: ( for n holds S2.n = a * S.n );
for n holds S1.n = S2.n
proof
let n;
S1.n = a * S.n by A1;
hence thesis by A2;
end;
hence thesis by FUNCT_2:113;
end;
end;
definition let RNS;
let S;
attr S is convergent means
:Def9: ex g st for r st 0 < r ex m st for n st m <= n holds
||.(S.n) - g.|| < r;
end;
canceled 6;
theorem Th34:
S1 is convergent & S2 is convergent implies
S1 + S2 is convergent
proof
assume that
A1: S1 is convergent and
A2: S2 is convergent;
consider g1 such that
A3: for r st 0 < r ex m st for n st m <= n holds
||.(S1.n) - g1.|| < r by A1,Def9;
consider g2 such that
A4: for r st 0 < r ex m st for n st m <= n holds
||.(S2.n) - g2.|| < r by A2,Def9;
take g = g1 + g2;
let r; assume 0 < r;
then A5: 0< r/2 by SEQ_2:3;
then consider m1 such that
A6: for n st m1 <= n holds ||.(S1.n) - g1.|| < r/2 by A3;
consider m2 such that
A7: for n st m2 <= n holds ||.(S2.n) - g2.|| < r/2 by A4,A5;
take k = m1 + m2;
let n such that
A8: k <= n;
m1 <= m1 + m2 by NAT_1:37;
then m1 <= n by A8,AXIOMS:22;
then A9: ||.(S1.n) - g1.|| < r/2 by A6;
m2 <= k by NAT_1:37;
then m2 <= n by A8,AXIOMS:22;
then ||.(S2.n) - g2.|| < r/2 by A7;
then ||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| < r/2 + r/2
by A9,REAL_1:67;
then A10: ||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| < r by XCMPLX_1:66;
A11: ||.(S1 + S2).n - g.|| = ||.(S1.n) + (S2.n) - (g1+g2).|| by Def5
.= ||.(S1.n) + ((S2.n) - (g1+g2)).|| by RLVECT_1:42
.= ||.(S1.n) + (-(g1+g2) + (S2.n)).|| by RLVECT_1:def 11
.= ||.-(g1+g2) + ((S1.n) + (S2.n)).|| by RLVECT_1:def 6
.= ||.((-g1)+(-g2)) + ((S1.n) + (S2.n)).|| by RLVECT_1:45
.= ||.(S1.n) + ((-g1)+(-g2)) + (S2.n).|| by RLVECT_1:def 6
.= ||.((S1.n) + (-g1)) + (-g2) + (S2.n).|| by RLVECT_1:def 6
.= ||.(S1.n) - g1 + (-g2) + (S2.n).|| by RLVECT_1:def 11
.= ||.(S1.n)- g1 + ((S2.n) + -g2).|| by RLVECT_1:def 6
.= ||.(S1.n) - g1 + ((S2.n) - g2).|| by RLVECT_1:def 11;
||.(S1.n) - g1 + ((S2.n) - g2).|| <=
||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| by Def2;
hence ||.(S1 + S2).n - g.|| < r by A10,A11,AXIOMS:22;
end;
theorem Th35:
S1 is convergent & S2 is convergent implies
S1 - S2 is convergent
proof
assume that
A1: S1 is convergent and
A2: S2 is convergent;
consider g1 such that
A3: for r st 0 < r ex m st for n st m <= n holds
||.(S1.n) - g1.|| < r by A1,Def9;
consider g2 such that
A4: for r st 0 < r ex m st for n st m <= n holds
||.(S2.n) - g2.|| < r by A2,Def9;
take g = g1 - g2;
let r; assume 0 < r;
then A5: 0< r/2 by SEQ_2:3;
then consider m1 such that
A6: for n st m1 <= n holds ||.(S1.n) - g1.|| < r/2 by A3;
consider m2 such that
A7: for n st m2 <= n holds ||.(S2.n) - g2.|| < r/2 by A4,A5;
take k = m1 + m2;
let n such that
A8: k <= n;
m1 <= m1 + m2 by NAT_1:37;
then m1 <= n by A8,AXIOMS:22;
then A9: ||.(S1.n) - g1.|| < r/2 by A6;
m2 <= k by NAT_1:37;
then m2 <= n by A8,AXIOMS:22;
then ||.(S2.n) - g2.|| < r/2 by A7;
then ||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| < r/2 + r/2
by A9,REAL_1:67;
then A10: ||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| < r by XCMPLX_1:66;
A11: ||.(S1 - S2).n - g.|| = ||.((S1.n) - (S2.n)) - (g1 - g2).|| by Def6
.= ||.(((S1.n) - (S2.n)) - g1) + g2.|| by RLVECT_1:43
.= ||. ((S1.n) - (g1 + (S2.n))) + g2.|| by RLVECT_1:41
.= ||. (((S1.n) - g1 ) - (S2.n)) + g2.|| by RLVECT_1:41
.= ||. ((S1.n) - g1 ) - ((S2.n) - g2).|| by RLVECT_1:43;
||.((S1.n) - g1) - ((S2.n) - g2).|| <=
||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| by Th7;
hence ||.(S1 - S2).n - g.|| < r by A10,A11,AXIOMS:22;
end;
theorem Th36:
S is convergent implies
S - x is convergent
proof
assume S is convergent;
then consider g such that
A1: for r st 0 < r ex m st for n
st m <= n holds ||.(S.n) - g.|| < r by Def9;
take h = g - x;
let r; assume 0 < r;
then consider m1 such that
A2: for n st m1 <= n holds ||.(S.n) - g.|| < r by A1;
take k = m1;
let n; assume k <= n;
then A3: ||.(S.n) - g.|| < r by A2;
||.(S.n) - g.|| = ||.((S.n) - 0'(RNS)) - g.|| by RLVECT_1:26
.= ||.((S.n) - (x - x)) - g.|| by RLVECT_1:28
.= ||.(((S.n) - x) + x) - g.|| by RLVECT_1:43
.= ||.((S.n) - x) + (x - g).|| by RLVECT_1:42
.= ||.((S.n) - x) + ((-g) + x).|| by RLVECT_1:def 11
.= ||.((S.n) - x) + -h.|| by RLVECT_1:47
.= ||.((S.n) - x) - h.|| by RLVECT_1:def 11;
hence ||.(S - x).n - h.|| < r by A3,Def7;
end;
theorem Th37:
S is convergent implies
a * S is convergent
proof
assume S is convergent;
then consider g such that
A1: for r st 0 < r ex m st for n
st m <= n holds ||.(S.n) - g.|| < r by Def9;
take h = a * g;
A2: now assume
A3: a = 0;
let r; assume
0 < r;
then consider m1 such that
A4: for n st m1 <= n holds ||.(S.n) - g.|| < r by A1;
take k = m1;
let n; assume k <= n;
then A5: ||.(S.n) - g.|| < r by A4;
||.a * (S.n) - a * g.|| = ||.0 * (S.n) - 0'(RNS).|| by A3,RLVECT_1:23
.= ||.0'(RNS) - 0'(RNS).|| by RLVECT_1:23
.= ||.0'(RNS).|| by RLVECT_1:26
.= 0 by Def2;
then ||.a * (S.n) - h.|| < r by A5,Th8;
hence ||.(a * S).n - h.|| < r by Def8;
end;
now assume
A6: a <> 0;
then A7: 0 < abs(a) by ABSVALUE:6;
let r such that
A8: 0 < r;
A9: 0 <> abs(a) by A6,ABSVALUE:6;
0/abs(a) =0;
then 0 < r/abs(a) by A7,A8,REAL_1:73;
then consider m1 such that
A10: for n st m1 <= n holds ||.(S.n) - g.|| < r/abs(a) by A1;
take k = m1;
let n; assume k <= n;
then A11: ||.(S.n) - g.|| < r/abs(a) by A10;
A12: ||.(a * (S.n)) - (a * g).|| = ||.a * ((S.n) - g).|| by RLVECT_1:48
.= abs(a) * ||.(S.n) - g.|| by Def2;
abs(a) * (r/abs(a)) = abs(a) * (abs(a)" * r) by XCMPLX_0:def 9
.= abs(a) *abs(a)" * r by XCMPLX_1:4
.= 1 * r by A9,XCMPLX_0:def 7
.= r;
then ||.(a *(S.n)) - h.|| < r by A7,A11,A12,REAL_1:70;
hence ||.(a * S).n - h.|| < r by Def8;
end;
hence thesis by A2;
end;
definition let RNS;
let S;
func ||.S.|| -> Real_Sequence means
:Def10: for n holds it.n =||.(S.n).||;
existence
proof
deffunc F(Nat) = ||.(S.$1).||;
consider s being Real_Sequence such that A1:
for n holds s.n = F(n) from ExRealSeq;
take s;
thus thesis by A1;
end;
uniqueness
proof
let s,t be Real_Sequence;
assume
A2: ( for n holds s.n = ||.(S.n).|| ) &
( for n holds t.n = ||.(S.n).|| );
now let n;
s.n = ||.(S.n).|| by A2; hence
s.n = t.n by A2;
end;
hence thesis by FUNCT_2:113;
end;
end;
canceled;
theorem Th39:
S is convergent implies ||.S.|| is convergent
proof
assume S is convergent;
then consider g such that
A1: for r st 0 < r ex m st for n
st m <= n holds ||.(S.n) - g.|| < r by Def9;
now let r be real number;
A2: r is Real by XREAL_0:def 1;
assume 0 < r;
then consider m1 such that
A3: for n st m1 <= n holds ||.(S.n) - g.|| < r by A1,A2;
take k = m1;
now let n; assume
k <= n;
then A4: ||.(S.n) - g.|| < r by A3;
abs(||.(S.n).|| - ||.g.||) <= ||.(S.n) - g.|| by Th13;
then abs(||.(S.n).|| - ||.g.||) < r by A4,AXIOMS:22;
hence abs(||.S.||.n - ||.g.||) < r by Def10;
end;
hence for n st k <= n holds abs(||.S.||.n - ||.g.||) < r;
end;
hence thesis by SEQ_2:def 6;
end;
definition let RNS;
let S;
assume
A1: S is convergent;
func lim S -> Point of RNS means
:Def11: for r st 0 < r ex m st for n st m <= n
holds ||.(S.n) - it.|| < r;
existence by A1,Def9;
uniqueness
proof
for x , y st
( for r st 0 < r ex m st for n st m <= n holds ||.(S.n) - x.|| < r ) &
( for r st 0 < r ex m st for n st m <= n holds ||.(S.n) - y.|| < r )
holds x = y
proof
given x , y such that
A2: for r st 0 < r ex m st for n st m <= n holds ||.(S.n) - x.|| < r and
A3: for r st 0 < r ex m st for n st m <= n holds ||.(S.n) - y.|| < r and
A4: x <> y;
A5: ||.x - y.|| <> 0 by A4,Th10;
A6: 0 <= ||.x - y.|| by Th8;
then A7: 0/4 < ||.x - y.||/4 by A5,REAL_1:73;
then consider m1 such that
A8: for n st m1 <= n holds ||.(S.n) - x.|| < ||.x - y.||/4 by A2;
consider m2 such that
A9: for n st m2 <= n holds ||.(S.n) - y.|| < ||.x - y.||/4 by A3,A7;
A10: now assume
m1 <= m2;
then A11: ||.(S.m2) - x.|| < ||.x - y.||/4 by A8;
||.(S.m2) - y.|| < ||.x - y.||/4 by A9;
then ||.(S.m2) - x.|| + ||.(S.m2) - y.|| < ||.x - y.||/4 + ||.x - y.||/4
by A11,REAL_1:67;
then A12: ||.(S.m2) - x.|| + ||.(S.m2) - y.|| <= ||.x - y.||/2 by XCMPLX_1:72;
||.x - y.|| <= ||.x - (S.m2).|| + ||.(S.m2) - y.|| by Th14;
then ||.x - y.|| <= ||.(S.m2) - x.|| + ||.(S.m2) - y.|| by Th11;
then not ||.x - y.||/2 < ||.x - y.|| by A12,AXIOMS:22;
hence contradiction by A5,A6,SEQ_2:4;
end;
now assume m2 <= m1;
then A13: ||.(S.m1) - y.|| < ||.x - y.||/4 by A9;
||.(S.m1) - x.|| < ||.x - y.||/4 by A8;
then ||.(S.m1) - x.|| + ||.(S.m1) - y.|| < ||.x - y.||/4 + ||.x - y.||/4
by A13,REAL_1:67;
then A14: ||.(S.m1) - x.|| + ||.(S.m1) - y.|| <= ||.x - y.||/2 by XCMPLX_1:72;
||.x - y.|| <= ||.x - (S.m1).|| + ||.(S.m1) - y.|| by Th14;
then ||.x - y.|| <= ||.(S.m1) - x.|| + ||.(S.m1) - y.|| by Th11;
then not ||.x - y.||/2 < ||.x - y.|| by A14,AXIOMS:22;
hence contradiction by A5,A6,SEQ_2:4;
end;
hence contradiction by A10;
end;
hence thesis;
end;
end;
canceled;
theorem
S is convergent & lim S = g implies
( ||.S - g.|| is convergent & lim ||.S - g.|| = 0 )
proof
assume that
A1: S is convergent and
A2: lim S = g;
S - g is convergent by A1,Th36;
then A3: ||.S - g.|| is convergent by Th39;
now let r be real number;
A4: r is Real by XREAL_0:def 1;
assume 0 < r;
then consider m1 such that
A5: for n st m1 <= n holds ||.(S.n) - g.|| < r by A1,A2,A4,Def11;
take k = m1;
let n; assume
k <= n;
then ||.(S.n) - g.|| < r by A5;
then A6: ||.((S.n) - g ) - 0'(RNS).|| < r by RLVECT_1:26;
abs(||.(S.n) - g.|| - ||.0'(RNS).||) <= ||.((S.n) - g ) - 0'(RNS)
.||
by Th13;
then abs(||.(S.n) - g.|| - ||.0'(RNS).||) < r by A6,AXIOMS:22;
then abs((||.(S.n) - g.|| - 0)) < r by Def2;
then abs((||.(S - g).n.|| - 0)) < r by Def7;
hence abs((||.S - g.||.n - 0)) < r by Def10;
end;
hence thesis by A3,SEQ_2:def 7;
end;
theorem
S1 is convergent & S2 is convergent implies
lim (S1 + S2) = (lim S1) + (lim S2)
proof
assume that
A1: S1 is convergent and
A2: S2 is convergent;
A3: S1 + S2 is convergent by A1,A2,Th34;
set g1 = lim S1;
set g2 = lim S2;
set g = g1 + g2;
now let r; assume 0 < r;
then A4: 0< r/2 by SEQ_2:3;
then consider m1 such that
A5: for n st m1 <= n holds ||.(S1.n) - g1.|| < r/2 by A1,Def11;
consider m2 such that
A6: for n st m2 <= n holds ||.(S2.n) - g2.|| < r/2 by A2,A4,Def11;
take k = m1 + m2;
let n such that
A7: k <= n;
m1 <= m1 + m2 by NAT_1:37;
then m1 <= n by A7,AXIOMS:22;
then A8: ||.(S1.n) - g1.|| < r/2 by A5;
m2 <= k by NAT_1:37;
then m2 <= n by A7,AXIOMS:22;
then ||.(S2.n) - g2.|| < r/2 by A6;
then ||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| < r/2 + r/2
by A8,REAL_1:67;
then A9: ||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| < r by XCMPLX_1:66;
A10: ||.(S1 + S2).n - g.|| = ||.(S1.n) + (S2.n) - (g1+g2).|| by Def5
.= ||.(S1.n) + ((S2.n) - (g1+g2)).|| by RLVECT_1:42
.= ||.(S1.n) + (-(g1+g2) + (S2.n)).|| by RLVECT_1:def 11
.= ||.-(g1+g2) + ((S1.n) + (S2.n)).|| by RLVECT_1:def 6
.= ||.((-g1)+(-g2)) + ((S1.n) + (S2.n)).|| by RLVECT_1:45
.= ||.(S1.n) + ((-g1)+(-g2)) + (S2.n).|| by RLVECT_1:def 6
.= ||.((S1.n) + (-g1)) + (-g2) + (S2.n).|| by RLVECT_1:def 6
.= ||.(S1.n) - g1 + (-g2) + (S2.n).|| by RLVECT_1:def 11
.= ||.(S1.n)- g1 + ((S2.n) + -g2).|| by RLVECT_1:def 6
.= ||.(S1.n) - g1 + ((S2.n) - g2).|| by RLVECT_1:def 11;
||.(S1.n) - g1 + ((S2.n) - g2).|| <=
||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| by Def2;
hence ||.(S1 + S2).n - g.|| < r by A9,A10,AXIOMS:22;
end;
hence thesis by A3,Def11;
end;
theorem
S1 is convergent & S2 is convergent implies
lim (S1 - S2) = (lim S1) - (lim S2)
proof
assume that
A1: S1 is convergent and
A2: S2 is convergent;
A3: S1 - S2 is convergent by A1,A2,Th35;
set g1 = lim S1;
set g2 = lim S2;
set g = g1 - g2;
now let r; assume 0 < r;
then A4: 0< r/2 by SEQ_2:3;
then consider m1 such that
A5: for n st m1 <= n holds ||.(S1.n) - g1.|| < r/2 by A1,Def11;
consider m2 such that
A6: for n st m2 <= n holds ||.(S2.n) - g2.|| < r/2 by A2,A4,Def11;
take k = m1 + m2;
let n such that
A7: k <= n;
m1 <= m1 + m2 by NAT_1:37;
then m1 <= n by A7,AXIOMS:22;
then A8: ||.(S1.n) - g1.|| < r/2 by A5;
m2 <= k by NAT_1:37;
then m2 <= n by A7,AXIOMS:22;
then ||.(S2.n) - g2.|| < r/2 by A6;
then ||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| < r/2 + r/2
by A8,REAL_1:67;
then A9: ||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| < r by XCMPLX_1:66;
A10: ||.(S1 - S2).n - g.|| = ||.((S1.n) - (S2.n)) - (g1 - g2).|| by Def6
.= ||.(((S1.n) - (S2.n)) - g1) + g2.|| by RLVECT_1:43
.= ||. ((S1.n) - (g1 + (S2.n))) + g2.|| by RLVECT_1:41
.= ||. (((S1.n) - g1 ) - (S2.n)) + g2.|| by RLVECT_1:41
.= ||. ((S1.n) - g1 ) - ((S2.n) - g2).|| by RLVECT_1:43;
||.((S1.n) - g1) - ((S2.n) - g2).|| <=
||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| by Th7;
hence ||.(S1 - S2).n - g.|| < r by A9,A10,AXIOMS:22;
end;
hence thesis by A3,Def11;
end;
theorem
S is convergent implies
lim (S - x) = (lim S) - x
proof
assume
A1: S is convergent;
then A2: S - x is convergent by Th36;
set g = lim S;
set h = g - x;
now let r; assume 0 < r;
then consider m1 such that
A3: for n st m1 <= n holds ||.(S.n) - g.|| < r by A1,Def11;
take k = m1;
let n; assume k <= n;
then A4: ||.(S.n) - g.|| < r by A3;
||.(S.n) - g.|| = ||.((S.n) - 0'(RNS)) - g.|| by RLVECT_1:26
.= ||.((S.n) - (x - x)) - g.|| by RLVECT_1:28
.= ||.(((S.n) - x) + x) - g.|| by RLVECT_1:43
.= ||.((S.n) - x) + (x - g).|| by RLVECT_1:42
.= ||.((S.n) - x) + ((-g) + x).|| by RLVECT_1:def 11
.= ||.((S.n) - x) + -h.|| by RLVECT_1:47
.= ||.((S.n) - x) - h.|| by RLVECT_1:def 11;
hence ||.(S - x).n - h.|| < r by A4,Def7;
end;
hence thesis by A2,Def11;
end;
theorem
S is convergent implies
lim (a * S) = a * (lim S)
proof
assume
A1: S is convergent;
then A2: a * S is convergent by Th37;
set g = lim S;
set h = a * g;
A3: now assume
A4: a = 0;
let r; assume 0 < r;
then consider m1 such that
A5: for n st m1 <= n holds ||.(S.n) - g.|| < r by A1,Def11;
take k = m1;
let n; assume k <= n;
then A6: ||.(S.n) - g.|| < r by A5;
||.a * (S.n) - a * g.|| = ||.0 * (S.n) - 0'(RNS).|| by A4,RLVECT_1:23
.= ||.0'(RNS) - 0'(RNS).|| by RLVECT_1:23
.= ||.0'(RNS).|| by RLVECT_1:26
.= 0 by Def2;
then ||.a * (S.n) - h.|| < r by A6,Th8;
hence ||.(a * S).n - h.|| < r by Def8;
end;
now assume
A7: a <> 0;
then A8: 0 < abs(a) by ABSVALUE:6;
let r such that
A9: 0 < r;
A10: 0 <> abs(a) by A7,ABSVALUE:6;
0/abs(a) =0;
then 0 < r/abs(a) by A8,A9,REAL_1:73;
then consider m1 such that
A11: for n st m1 <= n holds ||.(S.n) - g.|| < r/abs(a) by A1,Def11;
take k = m1;
let n; assume k <= n;
then A12: ||.(S.n) - g.|| < r/abs(a) by A11;
A13: ||.(a * (S.n)) - (a * g).|| = ||.a * ((S.n) - g).|| by RLVECT_1:48
.= abs(a) * ||.(S.n) - g.|| by Def2;
abs(a) * (r/abs(a)) = abs(a) * (abs(a)" * r) by XCMPLX_0:def 9
.= abs(a) *abs(a)" * r by XCMPLX_1:4
.= 1 * r by A10,XCMPLX_0:def 7
.= r;
then ||.(a *(S.n)) - h.|| < r by A8,A12,A13,REAL_1:70;
hence ||.(a * S).n - h.|| < r by Def8;
end;
hence thesis by A2,A3,Def11;
end;