:: Banach Space of Bounded Real Sequences
:: by Yasumasa Suzuki
::
:: Received January 6, 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, SEQ_1, SUBSET_1, FUNCT_1, XXREAL_0, ORDINAL2, RELAT_1,
XXREAL_2, RSSPACE, TARSKI, XBOOLE_0, NAT_1, CARD_1, RLSUB_1, REAL_1,
RLVECT_1, VALUED_1, ARYTM_3, ALGSTR_0, COMPLEX1, SEQ_4, NORMSP_1,
STRUCT_0, SUPINF_2, ARYTM_1, ZFMISC_1, REALSET1, PRE_TOPC, MEMBER_1,
RSSPACE3, SEQ_2, FUNCOP_1, FUNCSDOM, FUNCT_2, LOPBAN_1, REWRITE1,
RSSPACE4, METRIC_1, RELAT_2, NORMSP_0, FUNCT_7, ASYMPT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, RELAT_1, PRE_TOPC,
DOMAIN_1, FUNCOP_1, REALSET1, XXREAL_0, XXREAL_2, XCMPLX_0, COMPLEX1,
REAL_1, ORDINAL1, NAT_1, STRUCT_0, ALGSTR_0, XREAL_0, NUMBERS, FUNCT_1,
RELSET_1, FUNCT_2, INTEGRA2, RLVECT_1, NORMSP_0, NORMSP_1, VALUED_1,
SEQ_1, SEQ_2, SEQ_4, RLSUB_1, PARTFUN1, RSSPACE, RSSPACE3, LOPBAN_1;
constructors REAL_1, COMPLEX1, REALSET1, RLSUB_1, INTEGRA2, RSSPACE3,
LOPBAN_1, RVSUM_1, SEQ_4, RELSET_1, BINOP_2, SEQ_2, SERIES_1, COMSEQ_2,
BINOP_1, SEQ_1, FUNCSDOM;
registrations SUBSET_1, RELAT_1, ORDINAL1, FUNCT_2, NUMBERS, XREAL_0,
MEMBERED, REALSET1, STRUCT_0, RLVECT_1, RFUNCT_1, SEQ_2, NORMSP_1,
RSSPACE3, VALUED_0, RSSPACE, VALUED_1, SEQ_4, NORMSP_0, RELSET_1, NAT_1,
SEQ_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions TARSKI, XBOOLE_0, NORMSP_1, XXREAL_2;
equalities XBOOLE_0, RLVECT_1, BINOP_1, REALSET1, STRUCT_0, ALGSTR_0,
VALUED_1, NORMSP_0, RSSPACE, SEQ_1, FUNCSDOM;
expansions TARSKI, XBOOLE_0, NORMSP_1, NORMSP_0, XXREAL_2;
theorems RELAT_1, TARSKI, ABSVALUE, ZFMISC_1, XBOOLE_0, NAT_1, FUNCOP_1,
SEQ_1, SEQ_2, SEQM_3, SEQ_4, FUNCT_1, FUNCT_2, RLVECT_1, RLSUB_1,
NORMSP_1, XREAL_0, XCMPLX_0, INTEGRA2, RSSPACE, RSSPACE3, RFUNCT_2,
RSSPACE2, LOPBAN_1, COMPLEX1, XREAL_1, XXREAL_0, VALUED_0, ORDINAL1,
MEASURE6, NORMSP_0;
schemes SEQ_1, FUNCT_2, XBOOLE_0;
begin :: The Banach Space of Bounded Real Sequences
Lm1: for rseq be Real_Sequence for K be Real st
(for n be Nat holds rseq.n <= K) holds upper_bound rng rseq <= K
proof
let rseq be Real_Sequence;
let K be Real such that
A1: for n be Nat holds rseq.n <= K;
now
let s be Real;
assume s in rng rseq;
then ex n be object st n in NAT & rseq.n=s by FUNCT_2:11;
hence s <=K by A1;
end;
hence thesis by SEQ_4:45;
end;
Lm2: for rseq be Real_Sequence st rseq is bounded
for n be Nat holds rseq.n <= upper_bound rng rseq
proof
let rseq be Real_Sequence;
assume rseq is bounded;
then rng rseq is real-bounded by MEASURE6:39;
then
A1: rng rseq is bounded_above;
let n be Nat;
A2: n in NAT by ORDINAL1:def 12;
NAT = dom rseq by FUNCT_2:def 1;
then rseq.n in rng rseq by FUNCT_1:3,A2;
hence thesis by A1,SEQ_4:def 1;
end;
definition
func the_set_of_BoundedRealSequences -> Subset of
Linear_Space_of_RealSequences means
:Def1:
for x being object holds x in it iff x
in the_set_of_RealSequences & seq_id x is bounded;
existence
proof
defpred P[object] means seq_id $1 is bounded;
consider IT being set such that
A1: for x being object holds x in IT iff x in the_set_of_RealSequences &
P[x] from XBOOLE_0:sch 1;
for x be object st x in IT holds x in the_set_of_RealSequences by A1;
then IT is Subset of the_set_of_RealSequences by TARSKI:def 3;
hence thesis by A1;
end;
uniqueness
proof
let X1,X2 be Subset of Linear_Space_of_RealSequences;
assume that
A2: for x being object holds x in X1 iff x in the_set_of_RealSequences &
seq_id(x) is bounded and
A3: for x being object holds x in X2 iff x in the_set_of_RealSequences &
seq_id(x) is bounded;
thus X1 c= X2
proof
let x be object;
assume x in X1;
then x in the_set_of_RealSequences & seq_id(x) is bounded by A2;
hence thesis by A3;
end;
let x be object;
assume x in X2;
then x in the_set_of_RealSequences & seq_id(x) is bounded by A3;
hence thesis by A2;
end;
end;
registration
cluster the_set_of_BoundedRealSequences -> non empty;
coherence
proof
seq_id Zeroseq is bounded;
hence thesis by Def1;
end;
cluster the_set_of_BoundedRealSequences -> linearly-closed;
coherence
proof
set W = the_set_of_BoundedRealSequences;
A1: for a be Real
for v be VECTOR of Linear_Space_of_RealSequences st v in
W holds a * v in W
proof
let a be Real;
let v be VECTOR of Linear_Space_of_RealSequences;
assume v in W;
then
A2: seq_id v is bounded by Def1;
seq_id(a*v) = a(#)seq_id(v) by RSSPACE:3;
then seq_id(a*v) is bounded by A2,SEQM_3:37;
hence thesis by Def1;
end;
for v,u be VECTOR of Linear_Space_of_RealSequences st v in
the_set_of_BoundedRealSequences & u in the_set_of_BoundedRealSequences holds v
+ u in the_set_of_BoundedRealSequences
proof
let v,u be VECTOR of Linear_Space_of_RealSequences;
assume v in W & u in W;
then
A3: seq_id v is bounded & seq_id u is bounded by Def1;
seq_id(v+u)=seq_id v+seq_id u by RSSPACE:2;
hence thesis by A3,Def1;
end;
hence thesis by A1,RLSUB_1:def 1;
end;
end;
Lm3: RLSStruct (# the_set_of_BoundedRealSequences, Zero_(
the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences), Add_(
the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences), Mult_(
the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences) #) is Subspace
of Linear_Space_of_RealSequences by RSSPACE:11;
registration
cluster RLSStruct (# the_set_of_BoundedRealSequences, Zero_(
the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences), Add_(
the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences), Mult_(
the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences) #) -> Abelian
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital;
coherence by RSSPACE:11;
end;
Lm4: RLSStruct (# the_set_of_BoundedRealSequences, Zero_(
the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences), Add_(
the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences), Mult_(
the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences) #) is Abelian
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital;
definition
func linfty_norm -> Function of the_set_of_BoundedRealSequences, REAL means
:Def2:
for x be object st x in the_set_of_BoundedRealSequences
holds it.x = upper_bound rng abs seq_id x;
existence
proof
deffunc F(object) = upper_bound rng abs seq_id($1);
A1: for z be object
st z in the_set_of_BoundedRealSequences holds F(z) in REAL
by XREAL_0:def 1;
ex f being Function of the_set_of_BoundedRealSequences,REAL st
for x being object st x in the_set_of_BoundedRealSequences
holds f.x = F(x) from FUNCT_2
:sch 2(A1);
hence thesis;
end;
uniqueness
proof
let NORM1,NORM2 be Function of the_set_of_BoundedRealSequences, REAL such
that
A2: for x be object st x in the_set_of_BoundedRealSequences
holds NORM1.x
= upper_bound rng abs seq_id x and
A3: for x be object st x in the_set_of_BoundedRealSequences
holds NORM2.x
= upper_bound rng abs seq_id x;
A4: for z be object st z in the_set_of_BoundedRealSequences holds NORM1.z =
NORM2 . z
proof
let z be object such that
A5: z in the_set_of_BoundedRealSequences;
NORM1.z = upper_bound rng abs seq_id(z) by A2,A5;
hence thesis by A3,A5;
end;
dom NORM1 = the_set_of_BoundedRealSequences & dom NORM2 =
the_set_of_BoundedRealSequences by FUNCT_2:def 1;
hence thesis by A4,FUNCT_1:2;
end;
end;
Lm5: for rseq be Real_Sequence st for n be Nat holds rseq.n=In(0,REAL)
holds rseq is bounded & upper_bound rng abs rseq = 0
proof
let rseq be Real_Sequence such that
A1: for n be Nat holds rseq.n=In(0,REAL);
A2: for n be Nat holds (abs rseq).n=0
proof
let n be Nat;
A3: (abs rseq).n = |.rseq.n.| by SEQ_1:12;
rseq.n=0 by A1;
hence thesis by A3,ABSVALUE:2;
end;
rng abs rseq c= {0}
proof
let y be object;
assume y in rng abs rseq;
then ex n be object st n in NAT & abs(rseq).n=y by FUNCT_2:11;
then y=0 by A2;
hence thesis by TARSKI:def 1;
end;
then
A4: rng abs rseq = {0} by ZFMISC_1:33;
rseq is constant by A1,VALUED_0:def 18;
hence thesis by A4,SEQ_4:9;
end;
Lm6: for rseq be Real_Sequence st rseq is bounded &
upper_bound rng abs rseq = 0 holds
for n be Nat holds rseq.n = 0
proof
let rseq be Real_Sequence such that
A1: rseq is bounded & upper_bound rng abs rseq = 0;
let n be Nat;
0 <= |.rseq.n.| by COMPLEX1:46;
then 0 <= abs(rseq).n by SEQ_1:12;
then (abs rseq).n =0 by A1,Lm2;
then |.rseq.n.| = 0 by SEQ_1:12;
hence thesis by ABSVALUE:2;
end;
theorem
for rseq be Real_Sequence holds rseq is bounded &
upper_bound rng abs rseq = 0
iff for n be Nat holds rseq.n = 0 by Lm5,Lm6;
registration
cluster NORMSTR (# the_set_of_BoundedRealSequences, Zero_(
the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences), Add_(
the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences), Mult_(
the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences), linfty_norm #)
-> Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital;
coherence by Lm4,RSSPACE3:2;
end;
definition
func linfty_Space -> non empty NORMSTR equals
NORMSTR (#
the_set_of_BoundedRealSequences, Zero_(the_set_of_BoundedRealSequences,
Linear_Space_of_RealSequences), Add_(the_set_of_BoundedRealSequences,
Linear_Space_of_RealSequences), Mult_(the_set_of_BoundedRealSequences,
Linear_Space_of_RealSequences), linfty_norm #);
coherence;
end;
theorem Th2:
the carrier of linfty_Space = the_set_of_BoundedRealSequences & (
for x be set holds x is VECTOR of linfty_Space iff x is Real_Sequence & seq_id
x is bounded ) & 0.linfty_Space = Zeroseq & ( for u be VECTOR of linfty_Space
holds u = seq_id u ) & ( for u,v be VECTOR of linfty_Space holds u+v =seq_id(u)
+seq_id(v) ) &
( for r be Real for u be VECTOR of linfty_Space holds r*u =r(#)
seq_id(u) ) & ( for u be VECTOR of linfty_Space holds -u = -seq_id u & seq_id(-
u) = -seq_id u ) & ( for u,v be VECTOR of linfty_Space holds u-v =seq_id(u)-
seq_id(v) ) & ( for v be VECTOR of linfty_Space holds seq_id v is bounded ) &
for v be VECTOR of linfty_Space holds ||.v.|| = upper_bound rng abs seq_id v
proof
set l1 =linfty_Space;
A1: 0.l1 = 0.Linear_Space_of_RealSequences by RSSPACE:def 10
.= Zeroseq;
A2: for x be set holds x is Element of l1 iff x is Real_Sequence & seq_id x
is bounded
proof
let x be set;
x in the_set_of_RealSequences iff x is Real_Sequence by FUNCT_2:8,66;
hence thesis by Def1;
end;
A3: for u,v be VECTOR of l1 holds u+v =seq_id u+seq_id v
proof
let u,v be VECTOR of l1;
reconsider u1=u, v1 = v as VECTOR of Linear_Space_of_RealSequences by Lm3,
RLSUB_1:10;
set L1=Linear_Space_of_RealSequences;
set W = the_set_of_BoundedRealSequences;
dom (the addF of L1) = [:the carrier of L1,the carrier of L1:] by
FUNCT_2:def 1;
then
A4: dom ((the addF of Linear_Space_of_RealSequences)||W) =[:W,W:] by RELAT_1:62
;
u+v =((the addF of Linear_Space_of_RealSequences)||W).[u,v] by
RSSPACE:def 8
.=u1+v1 by A4,FUNCT_1:47;
hence thesis by RSSPACE:2;
end;
A5: for r be Real for u be VECTOR of l1 holds r*u =r(#)seq_id u
proof
let r be Real;
let u be VECTOR of l1;
reconsider u1=u as VECTOR of Linear_Space_of_RealSequences by Lm3,
RLSUB_1:10;
set L1=Linear_Space_of_RealSequences;
set W = the_set_of_BoundedRealSequences;
dom (the Mult of L1) = [:REAL,the carrier of L1:] by FUNCT_2:def 1;
then
A6: dom ((the Mult of Linear_Space_of_RealSequences) | [:REAL,W:]) =[:
REAL,W:] by RELAT_1:62,ZFMISC_1:96;
reconsider r as Element of REAL by XREAL_0:def 1;
r*u =((the Mult of Linear_Space_of_RealSequences)|[:REAL,W:]).[r,u]
by RSSPACE:def 9
.=r*u1 by A6,FUNCT_1:47;
hence thesis by RSSPACE:3;
end;
A7: for u be VECTOR of l1 holds u = seq_id u
proof
let u be VECTOR of l1;
u is VECTOR of Linear_Space_of_RealSequences by Lm3,RLSUB_1:10;
hence thesis;
end;
A8: for u be VECTOR of l1 holds -u =-seq_id u & seq_id(-u)=-seq_id u
proof
let u be VECTOR of l1;
-u = (-1)*u by RLVECT_1:16
.= -seq_id u by A5;
hence thesis;
end;
for u,v be VECTOR of l1 holds u-v =seq_id u-seq_id v
proof
let u,v be VECTOR of l1;
thus u-v = seq_id u+seq_id(-v) by A3
.= seq_id u-seq_id v by A8;
end;
hence thesis by A2,A7,A3,A5,A8,A1,Def2;
end;
theorem Th3:
for x, y being Point of linfty_Space,
a be Real holds ( ||.x.|| =
0 iff x = 0.linfty_Space ) & 0 <= ||.x.|| & ||.x+y.|| <= ||.x.|| + ||.y.|| &
||. a*x .|| = |.a.| * ||.x.||
proof
let x, y be Point of linfty_Space;
let a be Real;
A1: for n be Nat holds (abs(a(#)seq_id x)).n =|.a.|*(abs(
seq_id x).n)
proof
let n be Nat;
(|.a(#)seq_id x.|).n =|.(a(#)seq_id x).n.| by SEQ_1:12
.=|.a*((seq_id x).n).| by SEQ_1:9
.=|.a.|*(|.(seq_id x).n.|) by COMPLEX1:65
.=|.a.|*(abs(seq_id x).n) by SEQ_1:12;
hence thesis;
end;
abs(seq_id x).1 =|.(seq_id x).1.| by SEQ_1:12;
then
A2: 0<= abs(seq_id x).1 by COMPLEX1:46;
A3: for n be Nat holds (abs seq_id(x+y)).n = |.((seq_id x).n)
+ ((seq_id y).n).|
proof
let n be Nat;
(abs seq_id(x+y)).n = (abs(seq_id(seq_id x+seq_id y))).n by Th2
.= |.(seq_id x+seq_id y).n.| by SEQ_1:12
.= |.((seq_id x).n)+((seq_id y).n).| by SEQ_1:7;
hence thesis;
end;
A4: for n be Nat holds (abs seq_id(x+y)).n <= (abs seq_id x).n +
(abs seq_id y).n
proof
let n be Nat;
|.(seq_id x).n + ((seq_id y).n).| <= |.(seq_id x).n.| + |.(
seq_id y).n.| by COMPLEX1:56;
then
(abs(seq_id(x+y))) .n <= |.(seq_id x).n.| + |.(seq_id y).n.| by A3;
then (abs seq_id(x+y)) .n <= (abs seq_id x).n + |.(seq_id y).n.| by
SEQ_1:12;
hence thesis by SEQ_1:12;
end;
A5: for n being Nat holds (abs(seq_id(x+y))).n <= ((abs seq_id x
) + (abs seq_id y)).n
proof
let n be Nat;
(abs seq_id x).n + (abs seq_id y).n =((abs seq_id x) + (abs seq_id y)
).n by SEQ_1:7;
hence thesis by A4;
end;
A6: now
assume
A7: x=0.linfty_Space;
A8: for n be Nat holds (seq_id x).n=0 by A7,Th2;
thus ||.x.|| = upper_bound rng abs seq_id x by Th2
.= 0 by A8,Lm5;
end;
seq_id x is bounded by Def1;
then
A9: 0 <= upper_bound rng abs seq_id x by A2,Lm2;
seq_id x is bounded by Def1;
then rng abs seq_id x is real-bounded by MEASURE6:39;
then
A10: rng abs seq_id x is bounded_above;
A11: now
A12: x in the_set_of_RealSequences by Def1;
assume
A13: ||.x.|| = 0;
||.x.|| = upper_bound rng abs seq_id x & seq_id x is bounded by Th2;
then for n be Nat holds 0 = (seq_id x).n by A13,Lm6;
hence x=0.linfty_Space by A12,Th2,RSSPACE:5;
end;
A14: seq_id y is bounded by Def1;
A15: seq_id x is bounded by Def1;
now
let n be Nat;
A16: (abs seq_id y).n <=upper_bound rng abs seq_id y by A14,Lm2;
(abs seq_id x + abs seq_id y).n = (abs seq_id x).n + (abs seq_id y).n
& (abs seq_id x).n <=upper_bound rng abs seq_id x by A15,Lm2,SEQ_1:7;
then
A17: ((abs seq_id x) + (abs seq_id y)).n <= upper_bound(rng abs seq_id x)
+ upper_bound rng abs seq_id y by A16,XREAL_1:7;
(abs seq_id(x+y)).n <= (abs seq_id x + abs seq_id y).n by A5;
hence
(abs seq_id(x+y)).n <= upper_bound rng abs seq_id x + upper_bound rng
abs seq_id y by A17,XXREAL_0:2;
end;
then
A18: upper_bound rng abs seq_id(x+y) <= upper_bound rng abs seq_id x +
upper_bound rng abs seq_id y by Lm1;
A19: ||.y.|| = upper_bound rng abs seq_id y &
upper_bound rng abs seq_id(x+y) = ||.x + y.||
by Th2;
||. a*x .|| = upper_bound rng abs seq_id(a*x) by Th2
.=upper_bound rng |.seq_id(a(#)seq_id x).| by Th2
.=upper_bound(rng (|.a.| (#) (abs seq_id x))) by A1,SEQ_1:9
.=upper_bound(|.a.|**rng abs seq_id x) by INTEGRA2:17
.=|.a.|*upper_bound rng abs seq_id x by A10,COMPLEX1:46,INTEGRA2:13
.=|.a.|*||.x.|| by Th2;
hence thesis by A11,A6,A9,A19,A18,Th2;
end;
registration
cluster linfty_Space -> reflexive discerning RealNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable;
coherence
by Th3;
end;
theorem
for vseq be sequence of linfty_Space st vseq is
Cauchy_sequence_by_Norm holds vseq is convergent
proof
let vseq be sequence of linfty_Space such that
A1: vseq is Cauchy_sequence_by_Norm;
defpred P[object,object] means ex i be Nat st $1=i & ex rseqi be
Real_Sequence st (for n be Nat holds rseqi.n=(seq_id(vseq.n)).i) &
rseqi is convergent & $2 = lim rseqi;
A2: for x be object st x in NAT ex y be object st y in REAL & P[x,y]
proof
let x be object;
assume x in NAT;
then reconsider i=x as Nat;
deffunc F(Nat) = (seq_id(vseq.$1)).i;
consider rseqi be Real_Sequence such that
A3: for n be Nat holds rseqi.n = F(n) from SEQ_1:sch 1;
reconsider lr = lim rseqi as Element of REAL by XREAL_0:def 1;
take lr;
now
let e be Real such that
A4: e > 0;
thus ex k be Nat st for m be Nat st k <= m holds
|.rseqi.m -rseqi.k.| < e
proof
consider k be Nat such that
A5: for n, m be Nat st n >= k & m >= k holds ||.(vseq.n
) - (vseq.m).|| < e by A1,A4,RSSPACE3:8;
take k;
let m be Nat such that
A6: k<=m;
seq_id((vseq.m)-(vseq.k)) is bounded by Def1;
then
A7: |.seq_id((vseq.m) - (vseq.k)).|.i <=
upper_bound rng |.seq_id((vseq.m)
- (vseq.k)).| by Lm2;
seq_id((vseq.m) - (vseq.k)) =seq_id(seq_id(vseq.m)-seq_id(vseq.k)
) by Th2
.= seq_id(vseq.m)+-seq_id(vseq.k);
then
(seq_id((vseq.m) - (vseq.k))).i =(seq_id(vseq.m)).i+(-seq_id(vseq
.k)).i by SEQ_1:7
.=(seq_id(vseq.m)).i+(-(seq_id(vseq.k)).i) by SEQ_1:10
.=(seq_id(vseq.m)).i-(seq_id(vseq.k)).i
.=rseqi.m -(seq_id(vseq.k)).i by A3
.=rseqi.m - rseqi.k by A3;
then
A8: |.rseqi.m-rseqi.k.| = abs(seq_id((vseq.m) - (vseq.k))).i by SEQ_1:12;
||.(vseq.m) - (vseq.k).|| =
upper_bound rng |.seq_id((vseq.m) - (vseq.k)
).| by Th2;
then upper_bound rng |.seq_id((vseq.m) - (vseq.k)).| < e by A5,A6;
hence thesis by A7,A8,XXREAL_0:2;
end;
end;
then rseqi is convergent by SEQ_4:41;
hence thesis by A3;
end;
consider f be sequence of REAL such that
A9: for x be object st x in NAT holds P[x,f.x] from FUNCT_2:sch 1(A2);
reconsider tseq=f as Real_Sequence;
A10: now
let i be Nat;
reconsider x=i as set;
i in NAT by ORDINAL1:def 12;
then
ex i0 be Nat st x=i0 & ex rseqi be Real_Sequence st ( for
n be Nat holds rseqi.n=(seq_id(vseq.n)).i0 ) & rseqi is convergent &
f.x=lim rseqi by A9;
hence
ex rseqi be Real_Sequence st ( for n be Nat holds rseqi.n=
(seq_id(vseq.n)).i ) & rseqi is convergent & tseq.i=lim rseqi;
end;
A11: for e be Real st e >0
ex k be Nat st for n be Nat
st n >= k holds abs(seq_id tseq-seq_id(vseq.n)) is bounded &
upper_bound rng |.seq_id
tseq-seq_id(vseq.n).| <= e
proof
let e be Real such that
A12: e > 0;
reconsider e as Real;
consider k be Nat such that
A13: for n, m be Nat st n >= k & m >= k holds ||.(vseq.n) -
(vseq.m).|| < e by A1,A12,RSSPACE3:8;
A14: for m,n be Nat st n >= k & m >= k holds abs seq_id((vseq.n
) - (vseq.m)) is bounded &
upper_bound rng abs seq_id((vseq.n) - (vseq.m)) < e
proof
let m,n be Nat;
assume n >= k & m >= k;
then
A15: ||.(vseq.n) - (vseq.m).|| < e by A13;
seq_id((vseq.n) - (vseq.m)) is bounded by Def1;
hence thesis by A15,Def2;
end;
A16: for n be Nat for i be Nat holds for rseq be
Real_Sequence st ( for m be Nat holds rseq.m=|.seq_id(vseq.m-vseq.
n).|.i ) holds rseq is convergent &
lim rseq = abs((seq_id tseq -seq_id(vseq.n))
).i
proof
let n be Nat;
A17: for m,k be Nat holds seq_id((vseq.m) - (vseq.k)) =
seq_id(vseq.m)-seq_id(vseq.k)
proof
let m,k be Nat;
seq_id((vseq.m) - (vseq.k)) = seq_id(seq_id(vseq.m)-seq_id(vseq.k
)) by Th2;
hence thesis;
end;
now
let i be Nat;
consider rseqi be Real_Sequence such that
A18: for n be Nat holds rseqi.n=(seq_id(vseq.n)).i and
A19: rseqi is convergent & tseq.i=lim rseqi by A10;
now
let rseq be Real_Sequence such that
A20: for m be Nat holds rseq.m=abs(seq_id(vseq.m-vseq .n)).i;
A21: now
let m be Nat;
A22: seq_id(vseq.m - vseq.n) = seq_id(vseq.m)-seq_id(vseq.n) by A17;
thus rseq.m=abs(seq_id(vseq.m-vseq.n)).i by A20
.=|.(seq_id(vseq.m-vseq.n)).i.| by SEQ_1:12
.=|.(seq_id(vseq.m)).i -(seq_id(vseq.n)).i.| by A22,RFUNCT_2:1
.=|.(rseqi.m) -(seq_id(vseq.n)).i.| by A18;
end;
|.tseq.i-(seq_id(vseq.n)).i.|
= |.(tseq-(seq_id(vseq.n))).i.| by RFUNCT_2:1
.= abs((seq_id tseq -seq_id(vseq.n))).i by SEQ_1:12;
hence
rseq is convergent & lim rseq = abs(seq_id tseq -seq_id(vseq.n)
).i by A19,A21,RSSPACE3:1;
end;
hence
for rseq be Real_Sequence st ( for m be Nat holds rseq
.m=abs(seq_id(vseq.m-vseq.n)).i ) holds rseq is convergent & lim rseq = abs(
seq_id tseq -seq_id(vseq.n)).i;
end;
hence thesis;
end;
for n be Nat st n >= k holds abs(seq_id tseq-seq_id(vseq.n
)) is bounded & upper_bound rng |.seq_id tseq-seq_id(vseq.n).| <= e
proof
let n be Nat such that
A23: n >= k;
A24: for i be Nat holds abs((seq_id tseq -seq_id(vseq.n))).i <= e
proof
let i be Nat;
deffunc F(Nat)= abs(seq_id((vseq.$1) - (vseq.n))).i;
consider rseq be Real_Sequence such that
A25: for m be Nat holds rseq.m = F(m) from SEQ_1:sch 1;
A26: for m be Nat st m >= k holds rseq.m <= e
proof
let m be Nat;
A27: rseq.m = abs(seq_id((vseq.m) - (vseq.n))).i by A25;
assume
A28: m >= k;
then abs(seq_id((vseq.m) - (vseq.n))) is bounded by A14,A23;
then
A29: abs(seq_id((vseq.m) - (vseq.n))).i <=
upper_bound rng abs seq_id((vseq.m
) - (vseq.n)) by Lm2;
upper_bound rng abs seq_id((vseq.m) - (vseq.n)) <= e by A14,A23,A28;
hence thesis by A29,A27,XXREAL_0:2;
end;
rseq is convergent & lim rseq = abs(seq_id tseq-seq_id(vseq.n)).i
by A16,A25;
hence thesis by A26,RSSPACE2:5;
end;
A30: 0 + e < 1 + e by XREAL_1:8;
now
let i be Nat;
abs((seq_id tseq -seq_id(vseq.n))).i <= e & abs ((seq_id tseq -
seq_id(vseq.n ))).i =|.((seq_id tseq -seq_id(vseq.n))).i.| by A24,SEQ_1:12;
hence |.((seq_id tseq -seq_id(vseq.n))).i.| <e+1 by A30,XXREAL_0:2;
end;
then seq_id tseq -seq_id(vseq.n) is bounded by A12,SEQ_2:3;
hence thesis by A24,Lm1;
end;
hence thesis;
end;
A31: seq_id tseq is bounded
proof
consider m be Nat such that
A32: for n be Nat st n >= m holds abs (seq_id tseq -seq_id(
vseq.n)) is bounded & upper_bound rng abs (seq_id tseq -seq_id(vseq.n))
<= 1 by A11;
A33: abs (seq_id tseq -seq_id(vseq.m)) is bounded by A32;
set d=abs seq_id tseq;
set b=abs seq_id(vseq.m);
set a=abs(seq_id tseq -seq_id(vseq.m));
A34: seq_id(vseq.m) is bounded by Def1;
A35: for i be Nat holds d.i <= (a+b).i
proof
let i be Nat;
A36: b.i=|.(seq_id(vseq.m)).i.| & d.i=|.(seq_id tseq).i.| by SEQ_1:12;
a.i = |.(seq_id tseq+-seq_id(vseq.m)).i.| by SEQ_1:12
.= |.(seq_id tseq).i+(-seq_id(vseq.m)).i.| by SEQ_1:7
.= |.(seq_id tseq).i+(-(seq_id(vseq.m)).i).| by SEQ_1:10
.=|.(seq_id tseq).i-(seq_id(vseq.m)).i.|;
then d.i-b.i <= a.i by A36,COMPLEX1:59;
then d.i-b.i+b.i<= a.i + b.i by XREAL_1:6;
hence thesis by SEQ_1:7;
end;
d is bounded
proof
reconsider r=upper_bound rng (a+b)+1 as Real;
b.1=|. (seq_id(vseq.m)).1.| by SEQ_1:12;
then
A37: 0<= b.1 by COMPLEX1:46;
A38: upper_bound( rng(a+b) ) +0 < upper_bound( rng(a+b) )+1 by XREAL_1:8;
A39: now
let i be Nat;
d.i <= (a+b).i & (a+b).i <= upper_bound rng (a+b) by A33,A34,A35,Lm2;
then
A40: d.i <= upper_bound rng (a+b) by XXREAL_0:2;
d.i=|.(seq_id tseq).i.| by SEQ_1:12;
hence |.(seq_id tseq).i.| <r by A38,A40,XXREAL_0:2;
end;
a.1=|.(seq_id tseq -seq_id(vseq.m)).1.| by SEQ_1:12;
then (a+b).1 =a.1 + b.1 & 0<= a.1 by COMPLEX1:46,SEQ_1:7;
then 0 <= upper_bound rng(a+b) by A33,A34,A37,Lm2;
then seq_id tseq is bounded by A39,SEQ_2:3;
hence thesis;
end;
hence thesis by SEQM_3:37;
end;
A41: tseq in the_set_of_RealSequences by FUNCT_2:8;
then reconsider tv=tseq as Point of linfty_Space by A31,Def1;
take tv;
let e1 be Real such that
A42: e1 > 0;
set e=e1/2;
consider m be Nat such that
A43: for n be Nat st n >= m holds |.seq_id tseq-seq_id(vseq
.n).| is bounded & upper_bound rng abs(seq_id tseq-seq_id(vseq.n)) <= e
by A11,A42,XREAL_1:215;
A44: e < e1 by A42,XREAL_1:216;
now
reconsider u=tseq as VECTOR of linfty_Space by A31,A41,Def1;
let n be Nat;
assume n >= m;
then
A45: upper_bound rng( abs(seq_id tseq-seq_id(vseq.n))) <= e by A43;
reconsider v=vseq.n as VECTOR of linfty_Space;
seq_id(u-v) = u-v by Th2;
then upper_bound rng abs seq_id(u-v) =
upper_bound rng abs(seq_id tseq-seq_id(vseq.n)) by Th2;
then
A46: (the normF of linfty_Space).(u-v) <= e by A45,Def2;
||.(vseq.n) - tv.|| =||.-(tv-(vseq.n)).|| by RLVECT_1:33
.=||.tv-(vseq.n).|| by NORMSP_1:2;
hence ||.(vseq.n) - tv.|| < e1 by A44,A46,XXREAL_0:2;
end;
hence thesis;
end;
begin
definition
let X be non empty set;
let Y be RealNormSpace;
let IT be Function of X, the carrier of Y;
attr IT is bounded means
:Def4:
ex K being Real st 0 <= K & for x being Element of X holds ||. IT.x .|| <= K;
end;
theorem Th5:
for X be non empty set for Y be RealNormSpace holds for f be
Function of X,the carrier of Y st (for x be Element of X holds f.x=0.Y) holds f
is bounded
proof
let X be non empty set;
let Y be RealNormSpace;
let f be Function of X,the carrier of Y such that
A1: for x be Element of X holds f.x=0.Y;
A2: now
let x be Element of X;
thus ||. f.x .|| = ||. 0.Y .|| by A1
.=0;
end;
take 0;
thus thesis by A2;
end;
registration
let X be non empty set;
let Y be RealNormSpace;
cluster bounded for Function of X,the carrier of Y;
existence
proof
set f=X --> 0.Y;
reconsider f as Function of X,the carrier of Y;
take f;
for x be Element of X holds f.x =0.Y by FUNCOP_1:7;
hence thesis by Th5;
end;
end;
definition
let X be non empty set;
let Y be RealNormSpace;
func BoundedFunctions(X,Y) -> Subset of RealVectSpace(X,Y) means
:Def5:
for
x being set holds x in it iff x is bounded Function of X,the carrier of Y;
existence
proof
A1: RealVectSpace(X,Y) = RLSStruct(#Funcs(X,the carrier of Y), (FuncZero(X
,Y)),FuncAdd(X,Y),FuncExtMult(X,Y)#) by LOPBAN_1:def 4;
defpred P[object] means $1 is bounded Function of X,the carrier of Y;
consider IT being set such that
A2: for x being object holds x in IT iff x in Funcs(X,the carrier of Y) &
P[x] from XBOOLE_0:sch 1;
take IT;
for x be object st x in IT holds x in Funcs(X,the carrier of Y) by A2;
hence IT is Subset of RealVectSpace(X,Y) by A1,TARSKI:def 3;
let x be set;
thus x in IT implies x is bounded Function of X,the carrier of Y by A2;
assume
A3: x is bounded Function of X,the carrier of Y;
then x in Funcs(X,the carrier of Y) by FUNCT_2:8;
hence thesis by A2,A3;
end;
uniqueness
proof
let X1,X2 be Subset of RealVectSpace(X,Y);
assume that
A4: for x being set holds x in X1 iff x is bounded Function of X,the
carrier of Y and
A5: for x being set holds x in X2 iff x is bounded Function of X,the
carrier of Y;
for x being object st x in X2 holds x in X1
proof
let x be object;
assume x in X2;
then x is bounded Function of X,the carrier of Y by A5;
hence thesis by A4;
end;
then
A6: X2 c= X1;
for x being object st x in X1 holds x in X2
proof
let x be object;
assume x in X1;
then x is bounded Function of X,the carrier of Y by A4;
hence thesis by A5;
end;
then X1 c= X2;
hence thesis by A6;
end;
end;
registration
let X be non empty set;
let Y be RealNormSpace;
cluster BoundedFunctions(X,Y) -> non empty;
coherence
proof
set f=X --> 0.Y;
reconsider f as Function of X,the carrier of Y;
for x be Element of X holds f.x =0.Y by FUNCOP_1:7;
then f is bounded by Th5;
hence thesis by Def5;
end;
end;
theorem Th6:
for X be non empty set for Y be RealNormSpace holds
BoundedFunctions(X,Y) is linearly-closed
proof
let X be non empty set;
let Y be RealNormSpace;
set W = BoundedFunctions(X,Y);
A1: RealVectSpace(X,Y) = RLSStruct(#Funcs(X,the carrier of Y), (FuncZero(X,Y
)),FuncAdd(X,Y),FuncExtMult(X,Y)#) by LOPBAN_1:def 4;
A2: for v,u be VECTOR of RealVectSpace(X,Y) st v in W & u in W holds v + u in W
proof
let v,u be VECTOR of RealVectSpace(X,Y) such that
A3: v in W and
A4: u in W;
reconsider f=v+u as Function of X,the carrier of Y by A1,FUNCT_2:66;
f is bounded
proof
reconsider v1=v as bounded Function of X, the carrier of Y by A3,Def5;
consider K2 be Real such that
A5: 0 <= K2 and
A6: for x be Element of X holds ||. v1.x .|| <= K2 by Def4;
reconsider u1=u as bounded Function of X, the carrier of Y by A4,Def5;
consider K1 be Real such that
A7: 0 <= K1 and
A8: for x be Element of X holds ||. u1.x .|| <= K1 by Def4;
take K3=K1+K2;
now
let x be Element of X;
||. u1.x .|| <= K1 & ||. v1.x .|| <= K2 by A8,A6;
then
A9: ||. u1.x .|| + ||. v1.x .|| <= K1 +K2 by XREAL_1:7;
||. f.x .|| =||. v1.x+u1.x .|| & ||. u1.x+v1.x .|| <= ||. u1.x
.||+ ||. v1.x .|| by LOPBAN_1:11,NORMSP_1:def 1;
hence ||. f.x .|| <= K3 by A9,XXREAL_0:2;
end;
hence thesis by A7,A5;
end;
hence thesis by Def5;
end;
for a be Real
for v be VECTOR of RealVectSpace(X,Y) st v in W holds a * v in W
proof
let a be Real;
let v be VECTOR of RealVectSpace(X,Y) such that
A10: v in W;
reconsider f=a*v as Function of X,the carrier of Y by A1,FUNCT_2:66;
f is bounded
proof
reconsider v1=v as bounded Function of X, the carrier of Y by A10,Def5;
reconsider a as Real;
consider K be Real such that
A11: 0 <= K and
A12: for x be Element of X holds ||. v1.x .|| <= K by Def4;
reconsider aK = |.a.|*K as Real;
take aK;
A13: now
let x be Element of X;
A14: 0 <=|.a.| by COMPLEX1:46;
||. f.x .|| =||. a*v1.x .|| & ||. a*v1.x .|| = |.a.|* ||. v1.x
.|| by LOPBAN_1:12,NORMSP_1:def 1;
hence ||. f.x .|| <= |.a.|* K by A12,A14,XREAL_1:64;
end;
0 <=|.a.| by COMPLEX1:46;
hence thesis by A11,A13;
end;
hence thesis by Def5;
end;
hence thesis by A2,RLSUB_1:def 1;
end;
theorem
for X be non empty set for Y be RealNormSpace holds RLSStruct (#
BoundedFunctions(X,Y), Zero_(BoundedFunctions(X,Y), RealVectSpace(X,Y)), Add_(
BoundedFunctions(X,Y), RealVectSpace(X,Y)), Mult_(BoundedFunctions(X,Y),
RealVectSpace(X,Y)) #) is Subspace of RealVectSpace(X,Y) by Th6,RSSPACE:11;
registration
let X be non empty set;
let Y be RealNormSpace;
cluster RLSStruct (# BoundedFunctions(X,Y), Zero_(BoundedFunctions(X,Y),
RealVectSpace(X,Y)), Add_(BoundedFunctions(X,Y), RealVectSpace(X,Y)), Mult_(
BoundedFunctions(X,Y), RealVectSpace(X,Y)) #) -> Abelian add-associative
right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital;
coherence by Th6,RSSPACE:11;
end;
definition
let X be non empty set;
let Y be RealNormSpace;
func R_VectorSpace_of_BoundedFunctions(X,Y) -> RealLinearSpace equals
RLSStruct (# BoundedFunctions(X,Y), Zero_(BoundedFunctions(X,Y), RealVectSpace(
X,Y)), Add_(BoundedFunctions(X,Y), RealVectSpace(X,Y)), Mult_(BoundedFunctions(
X,Y), RealVectSpace(X,Y)) #);
coherence;
end;
registration
let X be non empty set;
let Y be RealNormSpace;
cluster R_VectorSpace_of_BoundedFunctions(X,Y) -> strict;
coherence;
end;
theorem Th8:
for X be non empty set for Y be RealNormSpace for f,g,h be
VECTOR of R_VectorSpace_of_BoundedFunctions(X,Y) for f9,g9,h9 be bounded
Function of X,the carrier of Y st f9=f & g9=g & h9=h holds (h = f+g iff for x
be Element of X holds h9.x = f9.x + g9.x )
proof
let X be non empty set;
let Y be RealNormSpace;
let f,g,h be VECTOR of R_VectorSpace_of_BoundedFunctions(X,Y);
A1: R_VectorSpace_of_BoundedFunctions(X,Y) is Subspace of RealVectSpace(X,Y)
by Th6,RSSPACE:11;
then reconsider f1=f as VECTOR of RealVectSpace(X,Y) by RLSUB_1:10;
reconsider h1=h as VECTOR of RealVectSpace(X,Y) by A1,RLSUB_1:10;
reconsider g1=g as VECTOR of RealVectSpace(X,Y) by A1,RLSUB_1:10;
let f9,g9,h9 be bounded Function of X,the carrier of Y such that
A2: f9=f & g9=g & h9=h;
A3: now
assume
A4: h = f+g;
let x be Element of X;
h1=f1+g1 by A1,A4,RLSUB_1:13;
hence h9.x=f9.x+g9.x by A2,LOPBAN_1:11;
end;
now
assume for x be Element of X holds h9.x=f9.x+g9.x;
then h1=f1+g1 by A2,LOPBAN_1:11;
hence h =f+g by A1,RLSUB_1:13;
end;
hence thesis by A3;
end;
theorem Th9:
for X be non empty set for Y be RealNormSpace for f,h be VECTOR
of R_VectorSpace_of_BoundedFunctions(X,Y) for f9,h9 be bounded Function of X,
the carrier of Y st f9=f & h9=h
for a be Real holds h = a*f iff for x be
Element of X holds h9.x = a*f9.x
proof
let X be non empty set;
let Y be RealNormSpace;
let f,h be VECTOR of R_VectorSpace_of_BoundedFunctions(X,Y);
let f9,h9 be bounded Function of X,the carrier of Y such that
A1: f9=f & h9=h;
let a be Real;
reconsider a as Real;
A2: R_VectorSpace_of_BoundedFunctions(X,Y) is Subspace of RealVectSpace(X,Y)
by Th6,RSSPACE:11;
then reconsider f1=f, h1=h as VECTOR of RealVectSpace(X,Y) by RLSUB_1:10;
A3: now
assume
A4: h = a*f;
let x be Element of X;
h1=a*f1 by A2,A4,RLSUB_1:14;
hence h9.x=a*f9.x by A1,LOPBAN_1:12;
end;
now
assume for x be Element of X holds h9.x=a*f9.x;
then h1=a*f1 by A1,LOPBAN_1:12;
hence h =a*f by A2,RLSUB_1:14;
end;
hence thesis by A3;
end;
theorem Th10:
for X be non empty set for Y be RealNormSpace holds 0.
R_VectorSpace_of_BoundedFunctions(X,Y) =(X -->0.Y)
proof
let X be non empty set;
let Y be RealNormSpace;
R_VectorSpace_of_BoundedFunctions(X,Y) is Subspace of RealVectSpace(X,Y)
& 0.RealVectSpace(X,Y) =(X -->0.Y) by Th6,LOPBAN_1:13,RSSPACE:11;
hence thesis by RLSUB_1:11;
end;
definition
let X be non empty set;
let Y be RealNormSpace;
let f be object such that
A1: f in BoundedFunctions(X,Y);
func modetrans(f,X,Y) -> bounded Function of X,the carrier of Y equals
:Def7
:
f;
coherence by A1,Def5;
end;
definition
let X be non empty set;
let Y be RealNormSpace;
let u be Function of X,the carrier of Y;
func PreNorms(u) -> non empty Subset of REAL equals
the set of all ||.u.t.|| where t is
Element of X ;
coherence
proof
set x = the Element of X;
A1: now
let x be object;
now
assume x in the set of all ||.u.t.|| where t is Element of X ;
then ex t be Element of X st x=||.u.t.||;
hence x in REAL;
end;
hence x in the set of all ||.u.t.|| where t is Element of X
implies x in REAL;
end;
||.u.x.|| in the set of all ||.u.t.|| where t is Element of X ;
hence thesis by A1,TARSKI:def 3;
end;
end;
theorem Th11:
for X be non empty set for Y be RealNormSpace for g be bounded
Function of X,the carrier of Y holds PreNorms(g) is bounded_above
proof
let X be non empty set;
let Y be RealNormSpace;
let g be bounded Function of X,the carrier of Y;
consider K be Real such that
0 <= K and
A1: for x be Element of X holds ||. g.x .|| <= K by Def4;
take K;
let r be ExtReal;
assume r in PreNorms(g);
then ex t be Element of X st r=||.g.t.||;
hence r <=K by A1;
end;
theorem
for X be non empty set for Y be RealNormSpace for g be Function of X,
the carrier of Y holds g is bounded iff PreNorms(g) is bounded_above
proof
let X be non empty set;
let Y be RealNormSpace;
let g be Function of X,the carrier of Y;
now
reconsider K=upper_bound PreNorms(g) as Real;
assume
A1: PreNorms(g) is bounded_above;
A2: 0 <= K
proof
consider r0 be object such that
A3: r0 in PreNorms(g) by XBOOLE_0:def 1;
reconsider r0 as Real by A3;
now
let r be Real;
assume r in PreNorms(g);
then ex t be Element of X st r=||.g.t.||;
hence 0 <= r;
end;
then 0 <= r0 by A3;
hence thesis by A1,A3,SEQ_4:def 1;
end;
take K;
now
let t be Element of X;
||.g.t.|| in PreNorms(g);
hence ||.g.t.|| <= K by A1,SEQ_4:def 1;
end;
hence g is bounded by A2;
end;
hence thesis by Th11;
end;
definition
let X be non empty set;
let Y be RealNormSpace;
func BoundedFunctionsNorm(X,Y) -> Function of BoundedFunctions(X,Y), REAL
means
:Def9:
for x be object st x in BoundedFunctions(X,Y) holds it.x = upper_bound
PreNorms(modetrans(x,X,Y));
existence
proof
deffunc F(object) = upper_bound PreNorms(modetrans($1,X,Y));
A1: for z be object st z in BoundedFunctions(X,Y) holds F(z) in REAL
by XREAL_0:def 1;
ex f being Function of BoundedFunctions(X,Y),REAL st
for x being object st
x in BoundedFunctions(X,Y) holds f.x = F(x) from FUNCT_2:sch 2(A1);
hence thesis;
end;
uniqueness
proof
let NORM1,NORM2 be Function of BoundedFunctions(X,Y), REAL such that
A2: for x be object st x in BoundedFunctions(X,Y)
holds NORM1.x = upper_bound
PreNorms(modetrans(x,X,Y)) and
A3: for x be object st x in BoundedFunctions(X,Y)
holds NORM2.x = upper_bound
PreNorms(modetrans(x,X,Y));
A4: for z be object st z in BoundedFunctions(X,Y) holds NORM1.z = NORM2.z
proof
let z be object such that
A5: z in BoundedFunctions(X,Y);
NORM1.z = upper_bound PreNorms(modetrans(z,X,Y)) by A2,A5;
hence thesis by A3,A5;
end;
dom NORM1 = BoundedFunctions(X,Y) & dom NORM2 = BoundedFunctions(X,Y)
by FUNCT_2:def 1;
hence thesis by A4,FUNCT_1:2;
end;
end;
theorem Th13:
for X be non empty set for Y be RealNormSpace for f be bounded
Function of X,the carrier of Y holds modetrans(f,X,Y)=f
proof
let X be non empty set;
let Y be RealNormSpace;
let f be bounded Function of X,the carrier of Y;
f in BoundedFunctions(X,Y) by Def5;
hence thesis by Def7;
end;
theorem Th14:
for X be non empty set for Y be RealNormSpace for f be bounded
Function of X,the carrier of Y holds BoundedFunctionsNorm(X,Y).f =
upper_bound PreNorms
(f)
proof
let X be non empty set;
let Y be RealNormSpace;
let f be bounded Function of X,the carrier of Y;
reconsider f9=f as set;
f in BoundedFunctions(X,Y) by Def5;
hence BoundedFunctionsNorm(X,Y).f = upper_bound PreNorms(modetrans(f9,X,Y))
by Def9
.= upper_bound PreNorms(f) by Th13;
end;
definition
let X be non empty set;
let Y be RealNormSpace;
func R_NormSpace_of_BoundedFunctions(X,Y) -> non empty NORMSTR equals
NORMSTR (# BoundedFunctions(X,Y), Zero_(BoundedFunctions(X,Y), RealVectSpace(X,
Y)), Add_(BoundedFunctions(X,Y), RealVectSpace(X,Y)), Mult_(BoundedFunctions(X,
Y), RealVectSpace(X,Y)), BoundedFunctionsNorm(X,Y) #);
coherence;
end;
theorem Th15:
for X be non empty set for Y be RealNormSpace holds (X --> 0.Y)
= 0.R_NormSpace_of_BoundedFunctions(X,Y)
proof
let X be non empty set;
let Y be RealNormSpace;
(X --> 0.Y) =0.R_VectorSpace_of_BoundedFunctions(X,Y) by Th10
.=0.R_NormSpace_of_BoundedFunctions(X,Y);
hence thesis;
end;
theorem Th16:
for X be non empty set for Y be RealNormSpace for f being Point
of R_NormSpace_of_BoundedFunctions(X,Y) for g be bounded Function of X,the
carrier of Y st g=f holds for t be Element of X holds ||.g.t.|| <= ||.f.||
proof
let X be non empty set;
let Y be RealNormSpace;
let f being Point of R_NormSpace_of_BoundedFunctions(X,Y);
let g be bounded Function of X,the carrier of Y such that
A1: g=f;
A2: PreNorms(g) is non empty bounded_above by Th11;
now
let t be Element of X;
||.g.t.|| in PreNorms(g);
then ||.g.t.|| <= upper_bound PreNorms(g) by A2,SEQ_4:def 1;
hence ||.g.t.|| <= ||.f.|| by A1,Th14;
end;
hence thesis;
end;
theorem
for X be non empty set for Y be RealNormSpace for f being Point of
R_NormSpace_of_BoundedFunctions(X,Y) holds 0 <= ||.f.||
proof
let X be non empty set;
let Y be RealNormSpace;
let f being Point of R_NormSpace_of_BoundedFunctions(X,Y);
reconsider g=f as bounded Function of X,the carrier of Y by Def5;
consider r0 be object such that
A1: r0 in PreNorms(g) by XBOOLE_0:def 1;
reconsider r0 as Real by A1;
A2: PreNorms(g) is non empty bounded_above by Th11;
now
let r be Real;
assume r in PreNorms(g);
then ex t be Element of X st r=||.g.t.||;
hence 0 <= r;
end;
then 0 <= r0 by A1;
then 0 <=upper_bound PreNorms(g) by A2,A1,SEQ_4:def 1;
hence thesis by Th14;
end;
theorem Th18:
for X be non empty set for Y be RealNormSpace for f being Point
of R_NormSpace_of_BoundedFunctions(X,Y) st f = 0.
R_NormSpace_of_BoundedFunctions(X,Y) holds 0 = ||.f.||
proof
let X be non empty set;
let Y be RealNormSpace;
let f being Point of R_NormSpace_of_BoundedFunctions(X,Y) such that
A1: f = 0.R_NormSpace_of_BoundedFunctions(X,Y);
thus ||.f.|| = 0
proof
reconsider g=f as bounded Function of X, the carrier of Y by Def5;
set z = X --> 0.Y;
reconsider z as Function of X, the carrier of Y;
consider r0 be object such that
A2: r0 in PreNorms(g) by XBOOLE_0:def 1;
reconsider r0 as Real by A2;
A3: (for s be Real st s in PreNorms(g) holds s <= 0) implies upper_bound
PreNorms(g) <= 0 by SEQ_4:45;
A4: PreNorms(g) is non empty bounded_above by Th11;
A5: z=g by A1,Th15;
A6: now
let r be Real;
assume r in PreNorms(g);
then consider t be Element of X such that
A7: r=||.g.t.||;
||.g.t.|| = ||.0.Y.|| by A5,FUNCOP_1:7
.= 0;
hence 0 <= r & r <=0 by A7;
end;
then 0 <= r0 by A2;
then upper_bound PreNorms(g) = 0 by A6,A4,A2,A3,SEQ_4:def 1;
hence thesis by Th14;
end;
end;
theorem Th19:
for X be non empty set for Y be RealNormSpace for f,g,h be Point
of R_NormSpace_of_BoundedFunctions(X,Y) for f9,g9,h9 be bounded Function of X,
the carrier of Y st f9=f & g9=g & h9=h holds (h = f+g iff for x be Element of X
holds h9.x = f9.x + g9.x )
proof
let X be non empty set;
let Y be RealNormSpace;
let f,g,h be Point of R_NormSpace_of_BoundedFunctions(X,Y);
reconsider f1=f, g1=g, h1=h as VECTOR of R_VectorSpace_of_BoundedFunctions(X
,Y);
A1: h=f+g iff h1=f1+g1;
let f9,g9,h9 be bounded Function of X,the carrier of Y;
assume f9=f & g9=g & h9=h;
hence thesis by A1,Th8;
end;
theorem Th20:
for X be non empty set for Y be RealNormSpace for f,h be Point
of R_NormSpace_of_BoundedFunctions(X,Y) for f9,h9 be bounded Function of X,the
carrier of Y st f9=f & h9=h
for a be Real holds h = a*f iff for x be Element of
X holds h9.x = a*f9.x
proof
let X be non empty set;
let Y be RealNormSpace;
let f,h be Point of R_NormSpace_of_BoundedFunctions(X,Y);
let f9,h9 be bounded Function of X,the carrier of Y such that
A1: f9=f & h9=h;
reconsider h1=h as VECTOR of R_VectorSpace_of_BoundedFunctions(X,Y);
reconsider f1=f as VECTOR of R_VectorSpace_of_BoundedFunctions(X,Y);
let a be Real;
h=a*f iff h1=a*f1;
hence thesis by A1,Th9;
end;
theorem Th21:
for X be non empty set for Y be RealNormSpace for f, g being
Point of R_NormSpace_of_BoundedFunctions(X,Y)
for a be Real holds ( ||.f.|| = 0
iff f = 0.R_NormSpace_of_BoundedFunctions(X,Y) ) & ||.a*f.|| = |.a.| * ||.f.||
& ||.f+g.|| <= ||.f.|| + ||.g.||
proof
let X be non empty set;
let Y be RealNormSpace;
let f, g being Point of R_NormSpace_of_BoundedFunctions(X,Y);
let a be Real;
A1: now
assume
A2: f = 0.R_NormSpace_of_BoundedFunctions(X,Y);
thus ||.f.|| = 0
proof
reconsider g=f as bounded Function of X,the carrier of Y by Def5;
set z = X --> 0.Y;
reconsider z as Function of X, the carrier of Y;
consider r0 be object such that
A3: r0 in PreNorms(g) by XBOOLE_0:def 1;
reconsider r0 as Real by A3;
A4: (for s be Real st s in PreNorms(g) holds s <= 0) implies
upper_bound
PreNorms(g) <= 0 by SEQ_4:45;
A5: PreNorms(g) is non empty bounded_above by Th11;
A6: z=g by A2,Th15;
A7: now
let r be Real;
assume r in PreNorms(g);
then consider t be Element of X such that
A8: r=||.g.t.||;
||.g.t.|| = ||.0.Y.|| by A6,FUNCOP_1:7
.= 0;
hence 0 <= r & r <=0 by A8;
end;
then 0<=r0 by A3;
then upper_bound PreNorms(g) = 0 by A7,A5,A3,A4,SEQ_4:def 1;
hence thesis by Th14;
end;
end;
A9: ||.f+g.|| <= ||.f.|| + ||.g.||
proof
reconsider f1=f, g1=g, h1=f+g as bounded Function of X,the carrier of Y by
Def5;
A10: now
let t be Element of X;
||.f1.t.||<= ||.f.|| & ||.g1.t.||<= ||.g.|| by Th16;
then
A11: ||.f1.t.||+||.g1.t.|| <= ||.f.|| + ||.g.|| by XREAL_1:7;
||.h1.t.||= ||.f1.t+g1.t.|| & ||.f1.t+g1.t.|| <=||.f1.t.||+||.g1.t
.|| by Th19,NORMSP_1:def 1;
hence ||.h1.t.|| <= ||.f.|| + ||.g.|| by A11,XXREAL_0:2;
end;
A12: now
let r be Real;
assume r in PreNorms(h1);
then ex t be Element of X st r=||.h1.t.||;
hence r <= ||.f.|| + ||.g.|| by A10;
end;
(for s be Real st s in PreNorms(h1) holds s <= ||.f.|| + ||.g
.||) implies upper_bound PreNorms(h1) <= ||.f.|| + ||.g.|| by SEQ_4:45;
hence thesis by A12,Th14;
end;
A13: ||.a*f.|| = |.a.| * ||.f.||
proof
reconsider f1=f, h1=a*f as bounded Function of X, the carrier of Y by Def5;
A14: (for s be Real st s in PreNorms(h1) holds s <= |.a.|*||.f.||
) implies upper_bound PreNorms(h1) <= |.a.|*||.f.|| by SEQ_4:45;
A15: now
let t be Element of X;
A16: 0<= |.a.| by COMPLEX1:46;
||.h1.t.||= ||.a*f1.t.|| & ||.a*f1.t.|| =|.a.|*||.f1.t.|| by Th20,
NORMSP_1:def 1;
hence ||.h1.t.|| <= |.a.|*||.f.|| by A16,Th16,XREAL_1:64;
end;
A17: now
let r be Real;
assume r in PreNorms(h1);
then ex t be Element of X st r=||.h1.t.||;
hence r <= |.a.|*||.f.|| by A15;
end;
A18: now
per cases;
case
A19: a <> 0;
A20: now
let t be Element of X;
A21: |.a".| =|.1*a".| .=|. 1/a.| by XCMPLX_0:def 9
.=1/|.a.| by ABSVALUE:7
.=1*|.a.|" by XCMPLX_0:def 9
.=|.a.|";
h1.t=a*f1.t by Th20;
then
A22: a"*h1.t =( a"* a)*f1.t by RLVECT_1:def 7
.=1*f1.t by A19,XCMPLX_0:def 7
.=f1.t by RLVECT_1:def 8;
||.a"*h1.t.|| =|.a".|*||.h1.t.|| & 0<= |.a".| by COMPLEX1:46
,NORMSP_1:def 1;
hence ||.f1.t.|| <= |.a.|"*||.a*f.|| by A22,A21,Th16,XREAL_1:64;
end;
A23: now
let r be Real;
assume r in PreNorms(f1);
then ex t be Element of X st r=||.f1.t.||;
hence r <= |.a.|"*||.a*f.|| by A20;
end;
A24: ( for s be Real st s in PreNorms(f1) holds s <= |.a.|"*
||.a*f.|| ) implies upper_bound PreNorms(f1) <= |.a.|"*||.a*f.||
by SEQ_4:45;
BoundedFunctionsNorm(X,Y).(f) = upper_bound PreNorms(f1) & 0 <= |.a.|
by Th14,COMPLEX1:46;
then |.a.|*||.f.|| <=|.a.|*(|.a.|"*||.a*f.||) by A23,A24,XREAL_1:64;
then
A25: |.a.|*||.f.|| <=(|.a.|*|.a.|")*||.a*f.||;
|.a.| <>0 by A19,COMPLEX1:47;
then |.a.|*||.f.|| <=1*||.a*f.|| by A25,XCMPLX_0:def 7;
hence |.a.|* ||.f.|| <=||.a*f.||;
end;
case
A26: a=0;
reconsider fz=f as VECTOR of R_VectorSpace_of_BoundedFunctions(X,Y);
A27: a*f =a*fz .=0.R_VectorSpace_of_BoundedFunctions(X,Y) by A26,RLVECT_1:10
.=0.R_NormSpace_of_BoundedFunctions(X,Y);
thus |.a.|* ||.f.|| =0 * ||.f.|| by A26,ABSVALUE:2
.=||.a*f.|| by A27,Th18;
end;
end;
BoundedFunctionsNorm(X,Y).(a*f) = upper_bound PreNorms(h1) by Th14;
hence thesis by A17,A14,A18,XXREAL_0:1;
end;
now
reconsider g=f as bounded Function of X,the carrier of Y by Def5;
set z = X --> 0.Y;
reconsider z as Function of X, the carrier of Y;
assume
A28: ||.f.|| = 0;
now
let t be Element of X;
||.g.t.|| <= ||.f.|| by Th16;
then ||.g.t.|| = 0 by A28;
hence g.t =0.Y by NORMSP_0:def 5
.=z.t by FUNCOP_1:7;
end;
then g=z by FUNCT_2:63;
hence f=0.R_NormSpace_of_BoundedFunctions(X,Y) by Th15;
end;
hence thesis by A1,A13,A9;
end;
theorem Th22:
for X be non empty set for Y be RealNormSpace holds
R_NormSpace_of_BoundedFunctions(X,Y) is
reflexive discerning RealNormSpace-like
by Th21;
theorem Th23:
for X be non empty set for Y be RealNormSpace holds
R_NormSpace_of_BoundedFunctions(X,Y) is RealNormSpace
proof
let X be non empty set;
let Y be RealNormSpace;
RLSStruct (# BoundedFunctions(X,Y), Zero_(BoundedFunctions(X,Y),
RealVectSpace(X,Y)), Add_(BoundedFunctions(X,Y), RealVectSpace(X,Y)), Mult_(
BoundedFunctions(X,Y), RealVectSpace(X,Y)) #) is RealLinearSpace;
hence thesis by Th22,RSSPACE3:2;
end;
registration
let X be non empty set;
let Y be RealNormSpace;
cluster R_NormSpace_of_BoundedFunctions(X,Y) ->
reflexive discerning RealNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable;
coherence by Th23;
end;
theorem Th24:
for X be non empty set for Y be RealNormSpace for f,g,h be Point
of R_NormSpace_of_BoundedFunctions(X,Y) for f9,g9,h9 be bounded Function of X,
the carrier of Y st f9=f & g9=g & h9=h holds (h = f-g iff for x be Element of X
holds h9.x = f9.x - g9.x )
proof
let X be non empty set;
let Y be RealNormSpace;
let f,g,h be Point of R_NormSpace_of_BoundedFunctions(X,Y);
let f9,g9,h9 be bounded Function of X,the carrier of Y such that
A1: f9=f & g9=g & h9=h;
A2: now
assume
A3: for x be Element of X holds h9.x = f9.x - g9.x;
now
let x be Element of X;
h9.x = f9.x - g9.x by A3;
then h9.x + g9.x= f9.x - (g9.x- g9.x) by RLVECT_1:29;
then h9.x + g9.x= f9.x - 0.Y by RLVECT_1:15;
hence h9.x + g9.x= f9.x;
end;
then f=h+g by A1,Th19;
then f-g=h+(g-g) by RLVECT_1:def 3;
then f-g=h+0.R_NormSpace_of_BoundedFunctions(X,Y) by RLVECT_1:15;
hence f-g=h;
end;
now
assume h=f-g;
then h+g=f-(g-g) by RLVECT_1:29;
then h+g=f-0.R_NormSpace_of_BoundedFunctions(X,Y) by RLVECT_1:15;
then
A4: h+g=f;
now
let x be Element of X;
f9.x=h9.x + g9.x by A1,A4,Th19;
then f9.x-g9.x=h9.x + (g9.x-g9.x) by RLVECT_1:def 3;
then f9.x-g9.x=h9.x + 0.Y by RLVECT_1:15;
hence f9.x-g9.x=h9.x;
end;
hence for x be Element of X holds h9.x = f9.x - g9.x;
end;
hence thesis by A2;
end;
Lm7: for e be Real, seq be Real_Sequence st ( seq is convergent & ex k be
Nat st for i be Nat st k <= i holds seq.i <=e ) holds lim
seq <=e
proof
let e be Real;
let seq be Real_Sequence such that
A1: seq is convergent and
A2: ex k be Nat st for i be Nat st k <= i holds
seq.i <=e;
consider k be Nat such that
A3: for i be Nat st k <= i holds seq.i <=e by A2;
reconsider ee=e as Element of REAL by XREAL_0:def 1;
set cseq = seq_const e;
A4: lim cseq = cseq.0 by SEQ_4:26
.= e by SEQ_1:57;
A5: now
let i be Nat;
reconsider ii=i as Element of NAT by ORDINAL1:def 12;
(seq ^\k).ii = seq.(k+ii) & seq.(k+i) <=e by A3,NAT_1:11,def 3;
hence (seq ^\k) .i <= cseq.i by SEQ_1:57;
end;
lim (seq ^\k)=lim seq by A1,SEQ_4:20;
hence thesis by A1,A5,A4,SEQ_2:18;
end;
theorem Th25:
for X be non empty set for Y be RealNormSpace st Y is complete
for seq be sequence of R_NormSpace_of_BoundedFunctions(X,Y) st seq is
Cauchy_sequence_by_Norm holds seq is convergent
proof
let X be non empty set;
let Y be RealNormSpace such that
A1: Y is complete;
let vseq be sequence of R_NormSpace_of_BoundedFunctions(X,Y) such that
A2: vseq is Cauchy_sequence_by_Norm;
defpred P[set, set] means ex xseq be sequence of Y st
(for n be Nat
holds xseq.n=modetrans((vseq.n),X,Y).$1) & xseq is convergent & $2= lim
xseq;
A3: for x be Element of X ex y be Element of Y st P[x,y]
proof
let x be Element of X;
deffunc F(Nat) = modetrans((vseq.$1),X,Y).x;
consider xseq be sequence of Y such that
A4: for n be Element of NAT holds xseq.n = F(n) from FUNCT_2:sch 4;
A5: for n be Nat holds xseq.n = F(n)
proof let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A4;
end;
take lim xseq;
A6: for m,k be Nat holds ||.xseq.m-xseq.k.|| <= ||.vseq.m -
vseq.k.||
proof
let m,k be Nat;
vseq.k is bounded Function of X,the carrier of Y by Def5;
then
A7: modetrans((vseq.k),X,Y)=vseq.k by Th13;
reconsider h1=vseq.m-vseq.k as bounded Function of X, the carrier of Y
by Def5;
vseq.m is bounded Function of X,the carrier of Y by Def5;
then
A8: modetrans((vseq.m),X,Y)=vseq.m by Th13;
m in NAT & k in NAT by ORDINAL1:def 12;
then xseq.m =modetrans((vseq.m),X,Y).x & xseq.k =modetrans((vseq.k),X,Y)
.x by A4;
then xseq.m - xseq.k = h1.x by A8,A7,Th24;
hence thesis by Th16;
end;
now
let e be Real such that
A9: e > 0;
thus ex k be Nat st for n, m be Nat st n >= k & m
>= k holds ||.xseq.n -xseq.m.|| < e
proof
consider k be Nat such that
A10: for n, m be Nat st n >= k & m >= k holds ||.(vseq.
n) - (vseq.m).|| < e by A2,A9,RSSPACE3:8;
take k;
thus for n, m be Nat st n >= k & m >= k holds ||.xseq.n-
xseq.m.|| < e
proof
let n,m be Nat;
assume n >=k & m >= k;
then
A11: ||.(vseq.n) - (vseq.m).|| < e by A10;
||.xseq.n-xseq.m.|| <= ||.(vseq.n) - (vseq.m).|| by A6;
hence thesis by A11,XXREAL_0:2;
end;
end;
end;
then xseq is Cauchy_sequence_by_Norm by RSSPACE3:8;
then xseq is convergent by A1,LOPBAN_1:def 15;
hence thesis by A5;
end;
consider f be Function of X,the carrier of Y such that
A12: for x be Element of X holds P[x,f.x] from FUNCT_2:sch 3(A3);
reconsider tseq=f as Function of X,the carrier of Y;
now
let e1 be Real such that
A13: e1 >0;
reconsider e =e1 as Real;
consider k be Nat such that
A14: for n, m be Nat st n >= k & m >= k holds ||.(vseq.n) -
(vseq.m).|| < e by A2,A13,RSSPACE3:8;
take k;
now
let m be Nat;
assume m >= k;
then
A15: ||.vseq.m.||= ||.vseq.||.m & ||.(vseq.m) - (vseq.k).|| <e by A14,
NORMSP_0:def 4;
|. ||.vseq.m.||- ||.vseq.k.|| .| <= ||.(vseq.m) - (vseq.k).|| & ||.
vseq.k .||= ||.vseq.||.k by NORMSP_0:def 4,NORMSP_1:9;
hence |. ||.vseq.||.m - ||.vseq.||.k .| <e1 by A15,XXREAL_0:2;
end;
hence
for m be Nat st m >= k holds |.||.vseq.||.m - ||.vseq.||
.k .| < e1;
end;
then
A16: ||.vseq.|| is convergent by SEQ_4:41;
A17: tseq is bounded
proof
reconsider lv = lim (||.vseq.|| ) as Real;
take lv;
A18: now
let x be Element of X;
consider xseq be sequence of Y such that
A19: for n be Nat holds xseq.n=modetrans((vseq.n),X,Y).x and
A20: xseq is convergent & tseq.x = lim xseq by A12;
A21: for m be Nat holds ||.xseq.m.|| <= ||.vseq.m.||
proof
let m be Nat;
vseq.m is bounded Function of X,the carrier of Y & xseq.m =
modetrans((vseq.m ),X,Y).x by A19,Def5;
hence thesis by Th13,Th16;
end;
A22: for n be Nat holds ||.xseq.||.n <=(||.vseq.||).n
proof
let n be Nat;
||.xseq.||.n = ||.(xseq.n).|| & ||.(xseq.n).|| <= ||.vseq.n.|| by A21,
NORMSP_0:def 4;
hence thesis by NORMSP_0:def 4;
end;
||.xseq.|| is convergent & ||.tseq.x.|| = lim ||.xseq.|| by A20,
LOPBAN_1:41;
hence ||.tseq.x.|| <= lim (||.vseq.|| ) by A16,A22,SEQ_2:18;
end;
now
let n be Nat;
||.vseq.n.|| >=0;
hence ||.vseq.||.n >=0 by NORMSP_0:def 4;
end;
hence thesis by A16,A18,SEQ_2:17;
end;
A23: for e be Real st e > 0 ex k be Nat st
for n be Nat st n >= k
holds for x be Element of X holds ||.modetrans((vseq.n),X,Y).x -
tseq.x.|| <= e
proof
let e be Real;
assume e > 0;
then consider k be Nat such that
A24: for n, m be Nat st n >= k & m >= k holds ||.(vseq.n) -
(vseq.m).|| < e by A2,RSSPACE3:8;
take k;
now
let n be Nat such that
A25: n >= k;
now
let x be Element of X;
consider xseq be sequence of Y such that
A26: for n be Nat holds xseq.n=modetrans((vseq.n),X,Y). x and
A27: xseq is convergent & tseq.x = lim xseq by A12;
A28: for m,k be Nat holds ||.xseq.m-xseq.k.|| <= ||.vseq.m
- vseq.k.||
proof
let m,k be Nat;
vseq.k is bounded Function of X,the carrier of Y by Def5;
then
A29: modetrans((vseq.k),X,Y)=vseq.k by Th13;
reconsider h1=vseq.m-vseq.k as bounded Function of X,the carrier of
Y by Def5;
vseq.m is bounded Function of X,the carrier of Y by Def5;
then
A30: modetrans((vseq.m),X,Y)=vseq.m by Th13;
xseq.m =modetrans((vseq.m),X,Y).x & xseq.k =modetrans((vseq.k),
X,Y).x by A26;
then xseq.m - xseq.k =h1.x by A30,A29,Th24;
hence thesis by Th16;
end;
A31: for m be Nat st m >=k holds ||.xseq.n-xseq.m.|| <= e
proof
let m be Nat;
assume m >=k;
then
A32: ||.vseq.n - vseq.m.|| <e by A24,A25;
||.xseq.n-xseq.m.|| <= ||.vseq.n - vseq.m.|| by A28;
hence thesis by A32,XXREAL_0:2;
end;
||.xseq.n-tseq.x.|| <= e
proof
deffunc F(Nat) = ||.xseq.$1 - xseq.n.||;
consider rseq be Real_Sequence such that
A33: for m be Nat holds rseq.m = F(m) from SEQ_1:sch
1;
now
let x be object;
assume x in NAT;
then reconsider k=x as Nat;
thus rseq.x = ||.xseq.k - xseq.n.|| by A33
.= ||.(xseq - xseq.n).k.|| by NORMSP_1:def 4
.= ||.(xseq - xseq.n).||.x by NORMSP_0:def 4;
end;
then
A34: rseq = ||.xseq - xseq.n.|| by FUNCT_2:12;
A35: xseq - xseq.n is convergent & lim (xseq-xseq.n)= tseq.x - xseq.
n by A27,NORMSP_1:21,27;
then
A36: lim rseq = ||.tseq.x-xseq.n.|| by A34,LOPBAN_1:20;
for m be Nat st m >= k holds rseq.m <= e
proof
let m be Nat such that
A37: m >=k;
rseq.m = ||.xseq.m-xseq.n.|| by A33
.= ||.xseq.n-xseq.m.|| by NORMSP_1:7;
hence thesis by A31,A37;
end;
then lim rseq <= e by A35,A34,Lm7,LOPBAN_1:20;
hence thesis by A36,NORMSP_1:7;
end;
hence ||.modetrans((vseq.n),X,Y).x - tseq.x.|| <= e by A26;
end;
hence for x be Element of X holds ||.modetrans((vseq.n),X,Y).x - tseq.x
.|| <= e;
end;
hence thesis;
end;
reconsider tseq as bounded Function of X,the carrier of Y by A17;
reconsider tv=tseq as Point of R_NormSpace_of_BoundedFunctions(X,Y) by Def5;
A38: for e be Real st e > 0 ex k be Nat st
for n be Nat st n >= k holds ||.vseq.n - tv.|| <= e
proof
let e be Real;
assume e > 0;
then consider k be Nat such that
A39: for n be Nat st n >= k holds for x be Element of X
holds ||.modetrans((vseq.n),X,Y).x - tseq.x.|| <= e by A23;
now
set g1=tseq;
let n be Nat such that
A40: n >= k;
reconsider h1=vseq.n-tv as bounded Function of X,the carrier of Y by Def5
;
set f1=modetrans((vseq.n),X,Y);
A41: now
let t be Element of X;
vseq.n is bounded Function of X,the carrier of Y by Def5;
then modetrans((vseq.n),X,Y)=vseq.n by Th13;
then ||.h1.t.||= ||.f1.t-g1.t.|| by Th24;
hence ||.h1.t.|| <=e by A39,A40;
end;
A42: now
let r be Real;
assume r in PreNorms(h1);
then ex t be Element of X st r=||.h1.t.||;
hence r <=e by A41;
end;
(for s be Real st s in PreNorms(h1) holds s <= e) implies
upper_bound PreNorms(h1) <=e by SEQ_4:45;
hence ||.vseq.n-tv.|| <=e by A42,Th14;
end;
hence thesis;
end;
for e be Real st e > 0 ex m be Nat st
for n be Nat st n >= m holds ||.(vseq.n) - tv.|| < e
proof
let e be Real such that
A43: e > 0;
reconsider ee=e as Real;
consider m be Nat such that
A44: for n be Nat st n >= m holds ||.(vseq.n) - tv.|| <= ee/
2 by A38,A43,XREAL_1:215;
A45: e/2<e by A43,XREAL_1:216;
now
let n be Nat;
assume n >= m;
then ||.(vseq.n) - tv.|| <= e/2 by A44;
hence ||.(vseq.n) - tv.|| < e by A45,XXREAL_0:2;
end;
hence thesis;
end;
hence thesis;
end;
theorem Th26:
for X be non empty set for Y be RealBanachSpace holds
R_NormSpace_of_BoundedFunctions(X,Y) is RealBanachSpace
proof
let X be non empty set;
let Y be RealBanachSpace;
for seq be sequence of R_NormSpace_of_BoundedFunctions(X,Y) st seq is
Cauchy_sequence_by_Norm holds seq is convergent by Th25;
hence thesis by LOPBAN_1:def 15;
end;
registration
let X be non empty set;
let Y be RealBanachSpace;
cluster R_NormSpace_of_BoundedFunctions (X,Y) -> complete;
coherence by Th26;
end;