:: Complex Banach Space of Bounded Complex Sequences
:: by Noboru Endou
::
:: Received March 18, 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, CSSPACE, RSSPACE, TARSKI, COMSEQ_1, ARYTM_3, REAL_1, CARD_1,
COMPLEX1, XCMPLX_0, VALUED_1, XBOOLE_0, RLSUB_1, RLVECT_1, CLVECT_1,
ALGSTR_0, SEQ_4, STRUCT_0, SUPINF_2, ARYTM_1, NORMSP_1, ZFMISC_1,
REALSET1, PRE_TOPC, MEMBER_1, NAT_1, RSSPACE3, SEQ_2, CLOPBAN1, FUNCOP_1,
FUNCT_2, LOPBAN_1, REWRITE1, CSSPACE4, NORMSP_0, METRIC_1, RELAT_2,
ASYMPT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, PRE_TOPC, DOMAIN_1,
RELAT_1, FUNCOP_1, REALSET1, XXREAL_0, XREAL_0, XXREAL_2, XCMPLX_0,
COMPLEX1, REAL_1, ORDINAL1, NAT_1, STRUCT_0, ALGSTR_0, NUMBERS, FUNCT_1,
RELSET_1, FUNCT_2, INTEGRA2, RLVECT_1, VALUED_1, COMSEQ_1, COMSEQ_2,
NORMSP_0, NORMSP_1, SEQ_1, SEQ_2, CLVECT_1, SEQ_4, PARTFUN1, CSSPACE,
CSSPACE3, CLOPBAN1;
constructors REAL_1, COMPLEX1, COMSEQ_2, REALSET1, INTEGRA2, LOPBAN_1,
CSSPACE3, CLOPBAN1, RVSUM_1, SEQ_4, RELSET_1, BINOP_2, SEQ_2, SERIES_1,
BINOP_1, SEQ_1, CFUNCDOM;
registrations SUBSET_1, RELAT_1, ORDINAL1, FUNCT_2, NUMBERS, XXREAL_0,
XREAL_0, MEMBERED, REALSET1, STRUCT_0, CLVECT_1, CSSPACE3, VALUED_0,
CSSPACE, VALUED_1, SEQ_2, SEQ_4, RFUNCT_1, NORMSP_0, RELSET_1, XCMPLX_0,
NAT_1, SEQ_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions TARSKI, XBOOLE_0, NORMSP_0, XXREAL_2;
equalities XBOOLE_0, REALSET1, CLOPBAN1, BINOP_1, STRUCT_0, ALGSTR_0,
VALUED_1, NORMSP_0, CSSPACE, CFUNCDOM;
expansions TARSKI, XBOOLE_0, CLOPBAN1, NORMSP_0, XXREAL_2;
theorems RELAT_1, TARSKI, ZFMISC_1, XBOOLE_0, NAT_1, FUNCOP_1, SEQ_1, SEQ_2,
SEQ_4, FUNCT_1, FUNCT_2, RLVECT_1, XREAL_0, XCMPLX_0, INTEGRA2, RSSPACE2,
CSSPACE, COMSEQ_2, COMPLEX1, CLVECT_1, COMSEQ_1, CSSPACE3, COMSEQ_3,
CLOPBAN1, XCMPLX_1, XREAL_1, XXREAL_0, LOPBAN_1, NORMSP_1, VALUED_1,
MEASURE6, NORMSP_0, ORDINAL1;
schemes SEQ_1, FUNCT_2, XBOOLE_0, COMSEQ_1;
begin :: Complex Banach space of bounded complex 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 holds
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_BoundedComplexSequences -> Subset of
Linear_Space_of_ComplexSequences means
:Def1:
for x being object holds x in it iff
x in the_set_of_ComplexSequences & 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_ComplexSequences
& P[x] from XBOOLE_0:sch 1;
for x be object st x in IT holds x in the_set_of_ComplexSequences by A1;
then IT is Subset of the_set_of_ComplexSequences by TARSKI:def 3;
hence thesis by A1;
end;
uniqueness
proof
let X1,X2 be Subset of Linear_Space_of_ComplexSequences;
assume that
A2: for x being object holds x in X1 iff x in the_set_of_ComplexSequences
& seq_id(x) is bounded and
A3: for x being object holds x in X2 iff x in the_set_of_ComplexSequences
& seq_id(x) is bounded;
thus X1 c= X2
proof
let x be object;
assume x in X1;
then x in the_set_of_ComplexSequences & 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_ComplexSequences & seq_id(x) is bounded by A3;
hence thesis by A2;
end;
end;
Lm3: for seq1,seq2 be Complex_Sequence st seq1 is bounded & seq2 is bounded
holds seq1 + seq2 is bounded
proof
let seq1,seq2 be Complex_Sequence;
assume that
A1: seq1 is bounded and
A2: seq2 is bounded;
consider r2 being Real such that
0 < r2 and
A3: for n be Nat holds |.seq2.n.| < r2 by A2,COMSEQ_2:8;
consider r1 being Real such that
0 < r1 and
A4: for n be Nat holds |.seq1.n.| < r1 by A1,COMSEQ_2:8;
for n be Nat holds |.(seq1+seq2).n.| < r1+r2
proof
let n be Nat;
A5: n in NAT by ORDINAL1:def 12;
|.(seq1+seq2).n.| = |.(seq1.n + seq2.n).| by VALUED_1:1,A5;
then
A6: |.(seq1+seq2).n.| <= |.seq1.n.| + |.seq2.n.| by COMPLEX1:56;
|.seq1.n.| < r1 by A4;
then |.seq1.n.| + |.seq2.n.| < r1 + r2 by A3,XREAL_1:8;
hence thesis by A6,XXREAL_0:2;
end;
hence thesis by COMSEQ_2:def 4;
end;
reconsider jj=1 as Real;
Lm4: for c be Complex, seq be Complex_Sequence st seq is bounded holds c(#)seq
is bounded
proof
let c be Complex;
let seq be Complex_Sequence;
assume seq is bounded;
then consider r be Real such that
0 < r and
A1: for n be Nat holds |.seq.n.| < r by COMSEQ_2:8;
ex r1 be Real st for n be Nat holds |.(c(#)seq).n.| < r1
proof
now
per cases;
case
A2: c = 0c;
take r1 = 1;
for n be Nat holds |.(c(#)seq).n.| < jj
proof
let n be Nat;
(c(#)seq).n = c * seq.n by VALUED_1:6
.= 0 by A2;
hence thesis by COMPLEX1:44;
end;
hence thesis;
end;
case
A3: c <> 0c;
take r1 = |.c.|*r;
for n be Nat holds |.(c(#)seq).n.| < |.c.|*r
proof
let n be Nat;
A4: |.(c(#)seq).n.| = |.c * seq.n.| by VALUED_1:6
.= |.c.|*|.seq.n.| by COMPLEX1:65;
|.c.| > 0 by A3,COMPLEX1:47;
hence thesis by A1,A4,XREAL_1:68;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis by COMSEQ_2:def 4;
end;
registration
cluster the_set_of_BoundedComplexSequences -> non empty;
coherence
proof
seq_id CZeroseq is bounded
proof
reconsider seq=seq_id CZeroseq as Complex_Sequence;
for n being Nat holds |.seq.n.| < jj by COMPLEX1:44
;
hence thesis by COMSEQ_2:8;
end;
hence thesis by Def1;
end;
cluster the_set_of_BoundedComplexSequences -> linearly-closed;
coherence
proof
set W = the_set_of_BoundedComplexSequences;
A1: for c be Complex, v be VECTOR of Linear_Space_of_ComplexSequences st v
in W holds c * v in W
proof
let c be Complex;
let v be VECTOR of Linear_Space_of_ComplexSequences;
assume v in W;
then
A2: seq_id v is bounded by Def1;
seq_id(c*v) =seq_id(c(#)seq_id(v)) by CSSPACE:3
.=c(#)seq_id(v);
then seq_id(c*v) is bounded by A2,Lm4;
hence thesis by Def1;
end;
for v,u be VECTOR of Linear_Space_of_ComplexSequences st v in
the_set_of_BoundedComplexSequences & u in the_set_of_BoundedComplexSequences
holds v + u in the_set_of_BoundedComplexSequences
proof
let v,u be VECTOR of Linear_Space_of_ComplexSequences;
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(seq_id v+seq_id u) by CSSPACE:2
.=seq_id v + seq_id u;
then seq_id(v+u) is bounded by A3,Lm3;
hence thesis by Def1;
end;
hence thesis by A1,CLVECT_1:def 7;
end;
end;
Lm5: CLSStruct (# the_set_of_BoundedComplexSequences, Zero_(
the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences), Add_(
the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences), Mult_(
the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences) #) is
Subspace of Linear_Space_of_ComplexSequences by CSSPACE:11;
registration
cluster CLSStruct (# the_set_of_BoundedComplexSequences, Zero_(
the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences), Add_(
the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences), Mult_(
the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences) #) ->
Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital;
coherence by CSSPACE:11;
end;
Lm6: CLSStruct (# the_set_of_BoundedComplexSequences, Zero_(
the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences), Add_(
the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences), Mult_(
the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences) #) is
Abelian add-associative right_zeroed right_complementable
vector-distributive scalar-distributive scalar-associative scalar-unital;
definition
func Complex_linfty_norm -> Function of the_set_of_BoundedComplexSequences,
REAL means
:Def2:
for x be object st x in the_set_of_BoundedComplexSequences holds
it.x = upper_bound rng |.seq_id x.|;
existence
proof
deffunc F(object) = upper_bound rng |.seq_id($1).|;
A1: for z be object st z in the_set_of_BoundedComplexSequences
holds F(z) in REAL by XREAL_0:def 1;
ex f being Function of the_set_of_BoundedComplexSequences,REAL st for x
being object st x in the_set_of_BoundedComplexSequences 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_BoundedComplexSequences, REAL
such that
A2: for x be object st x in the_set_of_BoundedComplexSequences holds
NORM1.x = upper_bound rng |.seq_id x.| and
A3: for x be object st x in the_set_of_BoundedComplexSequences holds
NORM2.x = upper_bound rng |.seq_id x.|;
A4: for z be object st z in the_set_of_BoundedComplexSequences holds NORM1.z
= NORM2.z
proof
let z be object such that
A5: z in the_set_of_BoundedComplexSequences;
NORM1.z = upper_bound rng |.seq_id(z).| by A2,A5;
hence thesis by A3,A5;
end;
dom NORM1 = the_set_of_BoundedComplexSequences & dom NORM2 =
the_set_of_BoundedComplexSequences by FUNCT_2:def 1;
hence thesis by A4,FUNCT_1:2;
end;
end;
Lm7: for seq be Complex_Sequence st (for n be Nat holds seq.n=0c)
holds seq is bounded & upper_bound rng |.seq.| = 0
proof
let seq be Complex_Sequence such that
A1: for n be Nat holds seq.n=0c;
for n be Nat holds |.seq.n.| < jj by A1,COMPLEX1:44;
hence seq is bounded by COMSEQ_2:def 4;
rng |.seq.| c= {0}
proof
let y be object;
assume y in rng |.seq.|;
then consider n be object such that
A2: n in NAT and
A3: (|.seq.|).n=y by FUNCT_2:11;
reconsider n as Nat by A2;
|.seq.| .n = |. seq.n .| by VALUED_1:18
.= |.0c.| by A1;
hence thesis by A3,COMPLEX1:44,TARSKI:def 1;
end;
then rng |.seq.| = {0} by ZFMISC_1:33;
hence thesis by SEQ_4:9;
end;
Lm8: for seq be Complex_Sequence st seq is bounded holds |.seq.| is bounded
proof
let seq be Complex_Sequence;
A1: 0 <= |. seq.0 .| by COMPLEX1:46;
assume seq is bounded;
then consider r be Real such that
A2: for n be Nat holds |.seq.n.| < r by COMSEQ_2:def 4;
A3: for n be Nat holds |.|.seq.| .n.| < r
proof
let n be Nat;
|.seq.| .n = |.seq.n.| by VALUED_1:18;
hence thesis by A2;
end;
|. seq.0 .| < r by A2;
hence thesis by A1,A3,SEQ_2:3;
end;
Lm9: for seq be Complex_Sequence st |.seq.| is bounded holds seq is bounded
proof
let seq be Complex_Sequence;
assume |.seq.| is bounded;
then consider r be Real such that
0 < r and
A1: for n be Nat holds |. |.seq.| .n.|<r by SEQ_2:3;
reconsider r as Real;
for n be Nat holds |.seq.n.| < r
proof
let n be Nat;
|.seq.| .n = |.seq.n.| by VALUED_1:18;
then |. |.seq.| .n.| = |.seq.n.|;
hence thesis by A1;
end;
hence thesis by COMSEQ_2:def 4;
end;
Lm10: for seq be Complex_Sequence st seq is bounded &
upper_bound rng |.seq.| = 0
holds for n be Nat holds seq.n = 0c
proof
let seq be Complex_Sequence such that
A1: seq is bounded and
A2: upper_bound rng |.seq.| = 0;
let n be Nat;
0 <= |.seq.n.| by COMPLEX1:46;
then
A3: 0 <= |.seq.| .n by VALUED_1:18;
|.seq.| is bounded by A1,Lm8;
then (|.seq.|).n =0 by A2,A3,Lm2;
then |.seq.n.| = 0 by VALUED_1:18;
hence thesis by COMPLEX1:45;
end;
theorem
for seq be Complex_Sequence holds seq is bounded &
upper_bound rng |.seq.| = 0
iff for n be Nat holds seq.n = 0c by Lm7,Lm10;
registration
cluster CNORMSTR (# the_set_of_BoundedComplexSequences, Zero_(
the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences), Add_(
the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences), Mult_(
the_set_of_BoundedComplexSequences,Linear_Space_of_ComplexSequences),
Complex_linfty_norm #) -> Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital;
coherence by Lm6,CSSPACE3:2;
end;
definition
func Complex_linfty_Space -> non empty CNORMSTR equals
CNORMSTR (#
the_set_of_BoundedComplexSequences, Zero_(the_set_of_BoundedComplexSequences,
Linear_Space_of_ComplexSequences), Add_(the_set_of_BoundedComplexSequences,
Linear_Space_of_ComplexSequences), Mult_(the_set_of_BoundedComplexSequences,
Linear_Space_of_ComplexSequences), Complex_linfty_norm #);
coherence;
end;
theorem Th2:
the carrier of Complex_linfty_Space =
the_set_of_BoundedComplexSequences & ( for x be set holds x is VECTOR of
Complex_linfty_Space iff x is Complex_Sequence & seq_id x is bounded ) & 0.
Complex_linfty_Space = CZeroseq & ( for u be VECTOR of Complex_linfty_Space
holds u = seq_id u ) & ( for u,v be VECTOR of Complex_linfty_Space holds u+v =
seq_id(u)+seq_id(v) ) & ( for c be Complex, u be VECTOR of Complex_linfty_Space
holds c*u =c(#)seq_id(u) ) & ( for u be VECTOR of Complex_linfty_Space holds -u
= -seq_id u & seq_id(-u) = -seq_id u ) & ( for u,v be VECTOR of
Complex_linfty_Space holds u-v =seq_id(u)-seq_id(v) ) & ( for v be VECTOR of
Complex_linfty_Space holds seq_id v is bounded ) & for v be VECTOR of
Complex_linfty_Space holds ||.v.|| = upper_bound rng |.seq_id v.|
proof
set l1 =Complex_linfty_Space;
A1: for x be set holds x is Element of l1 iff x is Complex_Sequence & seq_id
x is bounded
proof
let x be set;
x in the_set_of_ComplexSequences iff x is Complex_Sequence by FUNCT_2:8,66;
hence thesis by Def1;
end;
A2: 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_ComplexSequences by
Lm5,CLVECT_1:29;
set L1=Linear_Space_of_ComplexSequences;
set W = the_set_of_BoundedComplexSequences;
dom (the addF of L1) = [:the carrier of L1,the carrier of L1:] by
FUNCT_2:def 1;
then
A3: dom ((the addF of Linear_Space_of_ComplexSequences)||W) =[:W,W:] by
RELAT_1:62;
u+v =((the addF of Linear_Space_of_ComplexSequences)||W).[u,v] by
CSSPACE:def 8
.=u1+v1 by A3,FUNCT_1:47;
hence thesis by CSSPACE:2;
end;
A4: for c be Complex, u be VECTOR of l1 holds c*u =c(#)seq_id u
proof
let c be Complex;
let u be VECTOR of l1;
reconsider u1=u as VECTOR of Linear_Space_of_ComplexSequences by Lm5,
CLVECT_1:29;
set L1=Linear_Space_of_ComplexSequences;
set W = the_set_of_BoundedComplexSequences;
reconsider c as Element of COMPLEX by XCMPLX_0:def 2;
dom (the Mult of L1) = [:COMPLEX,the carrier of L1:] by FUNCT_2:def 1;
then
A5: dom ((the Mult of Linear_Space_of_ComplexSequences) | [:COMPLEX,W :])
=[:COMPLEX,W:] by RELAT_1:62,ZFMISC_1:96;
c*u =(the Mult of l1).[c,u] by CLVECT_1:def 1
.=((the Mult of Linear_Space_of_ComplexSequences)|[:COMPLEX,W:]).[c,u]
by CSSPACE:def 9
.=(the Mult of Linear_Space_of_ComplexSequences).[c,u] by A5,FUNCT_1:47
.=c*u1 by CLVECT_1:def 1;
hence thesis by CSSPACE:3;
end;
A6: 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_ComplexSequences by Lm5,CLVECT_1:29;
hence thesis;
end;
A7: 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 = (-1r)*u by CLVECT_1:3
.= (-1r)(#)seq_id u by A4
.= -seq_id u by COMSEQ_1:11;
hence thesis;
end;
A8: 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 A2
.= seq_id u-seq_id v by A7;
end;
A9: for v be VECTOR of l1 holds ||.v.|| = upper_bound rng |.seq_id v.|
by Def2;
0.l1 = 0.Linear_Space_of_ComplexSequences by CSSPACE:def 10
.= CZeroseq;
hence thesis by A1,A6,A2,A4,A7,A8,A9;
end;
theorem Th3:
for x, y being Point of Complex_linfty_Space, c be Complex holds
( ||.x.|| = 0 iff x = 0.Complex_linfty_Space ) & 0 <= ||.x.|| & ||.x+y.|| <=
||.x.|| + ||.y.|| & ||. c*x .|| = |.c.| * ||.x.||
proof
let x, y be Point of Complex_linfty_Space;
let c be Complex;
A1: for n be Nat holds (|.(c(#)seq_id x).|).n =|.c.|*(|.seq_id x
.|).n
proof
let n be Nat;
(|.c(#)seq_id x.|).n =|.((c(#)seq_id x).n).| by VALUED_1:18
.=|.(c*((seq_id x).n)).| by VALUED_1:6
.=|.c.|*(|.((seq_id x).n).|) by COMPLEX1:65
.=|.c.|*(|.(seq_id x).| .n) by VALUED_1:18;
hence thesis;
end;
|.seq_id x.| .1 =|.(seq_id x).1 .| by VALUED_1:18;
then
A2: 0<= |.seq_id x.| .1 by COMPLEX1:46;
A3: for n be Nat holds |.seq_id(x+y).| .n = |.(((seq_id x).n) +
((seq_id y).n)).|
proof
let n be Nat;
A4: n in NAT by ORDINAL1:def 12;
(|.seq_id(x+y).|).n = (|.(seq_id(seq_id x+seq_id y)).|).n by Th2
.= |.((seq_id x+seq_id y).n).| by VALUED_1:18
.= |.(((seq_id x).n)+((seq_id y).n)).| by VALUED_1:1,A4;
hence thesis;
end;
A5: for n be Nat holds (|.seq_id(x+y).|).n <= (|.seq_id x.|).n +
(|.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 (|.(seq_id(x+y)).|).n <= |.((seq_id x).n).| + |.((seq_id y).n).| by A3
;
then (|.seq_id(x+y).|).n <= (|.seq_id x.|).n + |.((seq_id y).n).| by
VALUED_1:18;
hence thesis by VALUED_1:18;
end;
A6: for n being Nat holds (|.(seq_id(x+y)).|).n <= ((|.seq_id x
.|) + (|.seq_id y.|)).n
proof
let n be Nat;
(|.seq_id x.|).n + (|.seq_id y.|).n =((|.seq_id x.|) + (|.seq_id y.|)
).n by SEQ_1:7;
hence thesis by A5;
end;
A7: now
A8: x in the_set_of_ComplexSequences by Def1;
assume
A9: ||.x.|| = 0;
||.x.|| = upper_bound rng |.seq_id x.| & seq_id x is bounded by Th2;
then for n be Nat holds 0c = (seq_id x).n by A9,Lm10;
hence x=0.Complex_linfty_Space by A8,Th2,CSSPACE:5;
end;
seq_id x is bounded by Def1;
then |.seq_id x.| is bounded by Lm8;
then
A10: 0 <= upper_bound rng |.seq_id x.| by A2,Lm2;
seq_id y is bounded by Def1;
then
A11: |.seq_id y.| is bounded by Lm8;
seq_id x is bounded by Def1;
then |.seq_id x.| is bounded by Lm8;
then rng |.seq_id x.| is real-bounded by MEASURE6:39;
then
A12: rng |.seq_id x.| is bounded_above;
A13: now
assume x=0.Complex_linfty_Space;
then
A14: for n be Nat holds (seq_id x).n=0c by Th2;
thus ||.x.|| = upper_bound rng |.seq_id x.| by Th2
.= 0 by A14,Lm7;
end;
seq_id x is bounded by Def1;
then
A15: |.seq_id x.| is bounded by Lm8;
now
let n be Nat;
A16: (|.seq_id y.|).n <=upper_bound rng |.seq_id y.| by A11,Lm2;
(|.seq_id x.| + |.seq_id y.|).n = (|.seq_id x.|).n + (|.seq_id y.|).n
& (|. seq_id x.|).n <=upper_bound rng |.seq_id x.| by A15,Lm2,SEQ_1:7;
then
A17: ((|.seq_id x.|) + (|.seq_id y.|)).n <= upper_bound rng |.seq_id x.| +
upper_bound rng |.seq_id y.| by A16,XREAL_1:7;
(|.seq_id(x+y).|).n <= (|.seq_id x.| + |.seq_id y.|).n by A6;
hence
(|.seq_id(x+y).|).n <= upper_bound rng |.seq_id x.| + upper_bound rng
|.seq_id y.| by A17,XXREAL_0:2;
end;
then
A18: upper_bound rng |.seq_id(x+y).| <= upper_bound rng |.seq_id x.| +
upper_bound rng |.seq_id y.| by Lm1;
A19: ||.y.|| = upper_bound rng |.seq_id y.| &
upper_bound rng |.seq_id(x+y).| = ||.x + y.||
by Th2;
||. c*x .|| = upper_bound rng |.seq_id(c*x).| by Th2
.=upper_bound rng |.(seq_id(c(#)seq_id x)).| by Th2
.=upper_bound(rng (|.c.| (#) (|.seq_id x.|))) by A1,SEQ_1:9
.=upper_bound(|.c.|**rng |.seq_id x.|) by INTEGRA2:17
.=|.c.|*upper_bound rng |.seq_id x.| by A12,COMPLEX1:46,INTEGRA2:13
.=|.c.|*||.x.|| by Th2;
hence thesis by A7,A13,A10,A19,A18,Th2;
end;
registration
cluster Complex_linfty_Space ->
reflexive discerning ComplexNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed
right_complementable;
coherence
by Th3,CLVECT_1:def 13;
end;
Lm11: for seq1,seq2,seq3 be Complex_Sequence holds seq1 = seq2 - seq3 iff for
n be Nat holds seq1.n = seq2.n - seq3.n
proof
let seq1,seq2,seq3 be Complex_Sequence;
A1: (for n be Nat holds seq1.n = seq2.n - seq3.n) implies seq1 =
seq2 - seq3
proof
assume
A2: for n be Nat holds seq1.n = seq2.n - seq3.n;
for x be object st x in NAT holds seq1.x = (seq2-seq3).x
proof
let x be object;
assume x in NAT;
then reconsider x as Element of NAT;
seq1.x = seq2.x - seq3.x by A2
.= seq2.x + -seq3.x
.= seq2.x + (-seq3).x by VALUED_1:8
.= (seq2 + (-seq3)).x by VALUED_1:1;
hence thesis;
end;
hence thesis by FUNCT_2:12;
end;
seq1 = seq2 - seq3 implies for n be Nat holds seq1.n = seq2.n
- seq3.n
proof
assume
A3: seq1 = seq2 - seq3;
now
let n be Nat;
A4: n in NAT by ORDINAL1:def 12;
seq1.n = seq2.n + (-seq3).n by A3,VALUED_1:1,A4
.= seq2.n + -seq3.n by VALUED_1:8;
hence seq1.n = seq2.n - seq3.n;
end;
hence thesis;
end;
hence thesis by A1;
end;
theorem Th4:
for vseq be sequence of Complex_linfty_Space st vseq is
Cauchy_sequence_by_Norm holds vseq is convergent
proof
let vseq be sequence of Complex_linfty_Space such that
A1: vseq is Cauchy_sequence_by_Norm;
defpred P[object,object] means ex i be Nat st $1=i & ex cseqi be
Complex_Sequence st (for n be Nat holds cseqi.n=(seq_id(vseq.n)).i)
& cseqi is convergent & $2 = lim cseqi;
A2: for x be object st x in NAT ex y be object st y in COMPLEX & 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 cseqi be Complex_Sequence such that
A3: for n be Nat holds cseqi.n = F(n) from COMSEQ_1:sch 1;
take lim cseqi;
thus lim cseqi in COMPLEX by XCMPLX_0:def 2;
now
let e be Real such that
A4: e > 0;
thus ex k be Nat st for m be Nat st k <= m holds
|.(cseqi.m -cseqi.k).| < e
proof
reconsider ee=e as Real;
consider k be Nat such that
A5: for n, m be Nat st n >= k & m >= k holds ||.(vseq.n
) - (vseq.m).|| < ee by A1,A4,CSSPACE3:8;
take k;
let m be Nat such that
A6: k<=m;
A7: i in NAT by ORDINAL1:def 12;
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 VALUED_1:1,A7
.=(seq_id(vseq.m)).i+(-(seq_id(vseq.k)).i) by VALUED_1:8
.=(seq_id(vseq.m)).i-(seq_id(vseq.k)).i
.=cseqi.m -(seq_id(vseq.k)).i by A3
.=cseqi.m - cseqi.k by A3;
then
A8: |.
(cseqi.m-cseqi.k).| = |.(seq_id((vseq.m)-(vseq.k))).| .i by VALUED_1:18;
seq_id((vseq.m)-(vseq.k)) is bounded by Def1;
then |.(seq_id((vseq.m)-(vseq.k))).| is bounded by Lm8;
then
A9: |.(seq_id((vseq.m) - (vseq.k))).| .i <=
upper_bound rng |.(seq_id((vseq.m
) - (vseq.k))).| by Lm2;
||.(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 A9,A8,XXREAL_0:2;
end;
end;
then cseqi is convergent by COMSEQ_3:46;
hence thesis by A3;
end;
consider f be sequence of COMPLEX such that
A10: for x be object st x in NAT holds P[x,f.x] from FUNCT_2:sch 1(A2);
reconsider tseq=f as Complex_Sequence;
A11: 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 cseqi be Complex_Sequence st (
for n be Nat holds cseqi.n=(seq_id(vseq.n)).i0 ) & cseqi is
convergent & f.x=lim cseqi by A10;
hence
ex cseqi be Complex_Sequence st ( for n be Nat holds cseqi
.n=(seq_id(vseq.n)).i ) & cseqi is convergent & tseq.i=lim cseqi;
end;
A12: for e be Real st e >0
ex k be Nat st for n be Nat
st n >= k holds |.(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
A13: e > 0;
consider k be Nat such that
A14: for n, m be Nat st n >= k & m >= k holds ||.(vseq.n) -
(vseq.m).|| < e by A1,A13,CSSPACE3:8;
A15: for m,n be Nat st n >= k & m >= k holds |.seq_id((vseq.n)
- (vseq.m)).| is bounded &
upper_bound rng |.seq_id((vseq.n) - (vseq.m)).| < e
proof
let m,n be Nat;
assume n >= k & m >= k;
then ||.(vseq.n) - (vseq.m).|| < e by A14;
then
A16: (the normF of Complex_linfty_Space).((vseq.n) - (vseq.m)) < e;
seq_id((vseq.n) - (vseq.m)) is bounded by Def1;
hence thesis by A16,Def2,Lm8;
end;
A17: 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 = |.((seq_id tseq -seq_id(vseq.n)
)).| .i
proof
let n be Nat;
A18: 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 cseqi be Complex_Sequence such that
A19: for n be Nat holds cseqi.n=(seq_id(vseq.n)).i and
A20: cseqi is convergent & tseq.i=lim cseqi by A11;
now
let rseq be Real_Sequence such that
A21: for m be Nat holds rseq.m=|.(seq_id(vseq.m-vseq. n)).| .i;
A22: now
let m be Nat;
A23: seq_id(vseq.m - vseq.n) = seq_id(vseq.m)-seq_id(vseq.n) by A18;
thus rseq.m=|.(seq_id(vseq.m-vseq.n)).| .i by A21
.=|.((seq_id(vseq.m-vseq.n)).i).| by VALUED_1:18
.=|.((seq_id(vseq.m)).i -(seq_id(vseq.n)).i).| by A23,Lm11
.= |.(cseqi.m -(seq_id(vseq.n)).i) .| by A19;
end;
|.(tseq.i-(seq_id(vseq.n)).i).| = |.((tseq-(seq_id(vseq.n))).i)
.| by Lm11
.= |.((seq_id tseq -seq_id(vseq.n))).| .i by VALUED_1:18;
hence
rseq is convergent & lim rseq = |.(seq_id tseq -seq_id(vseq.n))
.| .i by A20,A22,CSSPACE3:1;
end;
hence
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 = |.(
seq_id tseq -seq_id(vseq.n)).| .i;
end;
hence thesis;
end;
for n be Nat st n >= k holds |.(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
A24: n >= k;
A25: for i be Nat holds |.((seq_id tseq -seq_id(vseq.n))).| .
i <= e
proof
let i be Nat;
deffunc F(Nat)= |.(seq_id((vseq.$1) - (vseq.n))).| .i;
consider rseq be Real_Sequence such that
A26: for m be Nat holds rseq.m = F(m) from SEQ_1:sch 1;
A27: for m be Nat st m >= k holds rseq.m <= e
proof
let m be Nat;
A28: rseq.m = |.(seq_id((vseq.m) - (vseq.n))).| .i by A26;
assume
A29: m >= k;
then |.(seq_id((vseq.m) - (vseq.n))).| is bounded by A15,A24;
then
A30: |.(seq_id((vseq.m) - (vseq.n))).| .i <=
upper_bound rng |.seq_id((vseq.m
) - (vseq.n)).| by Lm2;
upper_bound rng |. seq_id((vseq.m) - (vseq.n)).| <= e by A15,A24,A29;
hence thesis by A30,A28,XXREAL_0:2;
end;
rseq is convergent & lim rseq = |.(seq_id tseq-seq_id(vseq.n)).|
.i by A17,A26;
hence thesis by A27,RSSPACE2:5;
end;
A31: 0 + e < 1 + e by XREAL_1:8;
now
let i be Nat;
|.((seq_id tseq -seq_id(vseq.n))).| .i <= e by A25;
then |.(((seq_id tseq -seq_id(vseq.n))).i).| <= e by VALUED_1:18;
hence |.(((seq_id tseq -seq_id(vseq.n))).i).| <e+1 by A31,XXREAL_0:2;
end;
then seq_id tseq -seq_id(vseq.n) is bounded by A13,COMSEQ_2:8;
hence thesis by A25,Lm1,Lm8;
end;
hence thesis;
end;
A32: seq_id tseq is bounded
proof
consider m be Nat such that
A33: for n be Nat st n >= m holds |.(seq_id tseq -seq_id(
vseq.n)).| is bounded & upper_bound rng |.(seq_id tseq -seq_id(vseq.n)).|
<= jj by A12;
A34: |.(seq_id tseq -seq_id(vseq.m)).| is bounded by A33;
set d=|.seq_id tseq.|;
set b=|.seq_id(vseq.m).|;
set a=|.(seq_id tseq -seq_id(vseq.m)).|;
seq_id(vseq.m) is bounded by Def1;
then
A35: |.seq_id (vseq.m).| is bounded by Lm8;
A36: for i be Nat holds d.i <= (a+b).i
proof
let i be Nat;
A37: i in NAT by ORDINAL1:def 12;
A38: b.i=|.((seq_id(vseq.m)).i).| & d.i=|.((seq_id tseq).i).| by VALUED_1:18;
a.i = |.((seq_id tseq+-seq_id(vseq.m)).i).| by VALUED_1:18
.= |.((seq_id tseq).i+(-seq_id(vseq.m)).i).| by VALUED_1:1,A37
.= |.((seq_id tseq).i+(-(seq_id(vseq.m)).i)).| by VALUED_1:8
.= |.((seq_id tseq).i-(seq_id(vseq.m)).i).|;
then d.i-b.i <= a.i by A38,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 VALUED_1:18;
then
A39: 0<= b.1 by COMPLEX1:46;
A40: upper_bound( rng(a+b) ) +0 < upper_bound( rng(a+b) )+1 by XREAL_1:8;
A41: now
let i be Nat;
d.i <= (a+b).i & (a+b).i <= upper_bound rng (a+b) by A34,A35,A36,Lm2;
then
A42: d.i <= upper_bound rng (a+b) by XXREAL_0:2;
d.i=|.((seq_id tseq).i).| by VALUED_1:18;
hence |.((seq_id tseq).i).| <r by A40,A42,XXREAL_0:2;
end;
a.1=|.((seq_id tseq -seq_id(vseq.m)).1).| by VALUED_1:18;
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 A34,A35,A39,Lm2;
then seq_id tseq is bounded by A41,COMSEQ_2:8;
hence thesis by Lm8;
end;
hence thesis by Lm9;
end;
A43: tseq in the_set_of_ComplexSequences by FUNCT_2:8;
then reconsider tv=tseq as Point of Complex_linfty_Space by A32,Def1;
ex tv be Point of Complex_linfty_Space st
for e1 be Real st e1 > 0 ex m
be Nat st for n be Nat st n >= m holds ||.(vseq.n) - tv
.|| < e1
proof
take tv;
let e1 be Real such that
A44: e1 > 0;
set e=e1/2;
reconsider ee=e as Real;
consider m be Nat such that
A45: for n be Nat st n >= m holds |.(seq_id tseq-seq_id(
vseq.n)).| is bounded & upper_bound rng |.(seq_id tseq-seq_id(vseq.n)).|
<= ee by A12,A44;
A46: e < e1 by A44,XREAL_1:216;
now
reconsider u=tseq as VECTOR of Complex_linfty_Space by A32,A43,Def1;
let n be Nat;
assume n >= m;
then
A47: upper_bound rng( |.(seq_id tseq-seq_id(vseq.n)).|) <= e by A45;
reconsider v=vseq.n as VECTOR of Complex_linfty_Space;
seq_id(u-v) = u-v by Th2;
then upper_bound rng |.seq_id(u-v).| =
upper_bound rng |.(seq_id tseq-seq_id(vseq.n)).|
by Th2;
then
A48: (the normF of Complex_linfty_Space).(u-v) <= e by A47,Def2;
||.(vseq.n) - tv.|| =||.-(tv-(vseq.n)).|| by RLVECT_1:33
.=||.tv-(vseq.n).|| by CLVECT_1:103;
then ||.(vseq.n) - tv.|| <= e by A48;
hence ||.(vseq.n) - tv.|| < e1 by A46,XXREAL_0:2;
end;
hence thesis;
end;
hence thesis by CLVECT_1:def 15;
end;
theorem
Complex_linfty_Space is ComplexBanachSpace by Th4,CLOPBAN1:def 13;
begin :: Another example of complex Banach space
definition
let X be non empty set;
let Y be ComplexNormSpace;
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 Th6:
for X be non empty set, Y be ComplexNormSpace, 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 ComplexNormSpace;
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 ComplexNormSpace;
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 Th6;
end;
end;
definition
let X be non empty set;
let Y be ComplexNormSpace;
func ComplexBoundedFunctions(X,Y) -> Subset of ComplexVectSpace(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
defpred P[object] means $1 is bounded Function of X,the carrier of Y;
consider IT being set such that
A1: 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 A1;
hence IT is Subset of ComplexVectSpace(X,Y) by TARSKI:def 3;
let x be set;
thus x in IT implies x is bounded Function of X,the carrier of Y by A1;
assume
A2: 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 A1,A2;
end;
uniqueness
proof
let X1,X2 be Subset of ComplexVectSpace(X,Y);
assume that
A3: for x being set holds x in X1 iff x is bounded Function of X,the
carrier of Y and
A4: 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 A4;
hence thesis by A3;
end;
then
A5: 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 A3;
hence thesis by A4;
end;
then X1 c= X2;
hence thesis by A5;
end;
end;
registration
let X be non empty set;
let Y be ComplexNormSpace;
cluster ComplexBoundedFunctions(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 Th6;
hence thesis by Def5;
end;
end;
theorem Th7:
for X be non empty set for Y be ComplexNormSpace holds
ComplexBoundedFunctions(X,Y) is linearly-closed
proof
let X be non empty set;
let Y be ComplexNormSpace;
set W = ComplexBoundedFunctions(X,Y);
A1: for v,u be VECTOR of ComplexVectSpace(X,Y) st v in W & u in W holds v +
u in W
proof
let v,u be VECTOR of ComplexVectSpace(X,Y) such that
A2: v in W and
A3: u in W;
reconsider f=v+u as Function of X,the carrier of Y by FUNCT_2:66;
f is bounded
proof
reconsider v1=v as bounded Function of X, the carrier of Y by A2,Def5;
consider K2 be Real such that
A4: 0 <= K2 and
A5: 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 A3,Def5;
consider K1 be Real such that
A6: 0 <= K1 and
A7: 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 A7,A5;
then
A8: ||. 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 CLOPBAN1:11,CLVECT_1:def 13;
hence ||. f.x .|| <= K3 by A8,XXREAL_0:2;
end;
hence thesis by A6,A4;
end;
hence thesis by Def5;
end;
for c be Complex for v be VECTOR of ComplexVectSpace(X,Y) st v in W
holds c * v in W
proof
let c be Complex;
let v be VECTOR of ComplexVectSpace(X,Y) such that
A9: v in W;
reconsider f=c*v as Function of X,the carrier of Y by FUNCT_2:66;
f is bounded
proof
reconsider v1=v as bounded Function of X, the carrier of Y by A9,Def5;
consider K be Real such that
A10: 0 <= K and
A11: for x be Element of X holds ||. v1.x .|| <= K by Def4;
take |.c.|*K;
A12: now
let x be Element of X;
A13: 0 <=|.c.| by COMPLEX1:46;
||. f.x .|| =||. c*v1.x .|| & ||. c*v1.x .|| = |.c.|* ||. v1.x
.|| by CLOPBAN1:12,CLVECT_1:def 13;
hence ||. f.x .|| <= |.c.|* K by A11,A13,XREAL_1:64;
end;
0 <=|.c.| by COMPLEX1:46;
hence thesis by A10,A12;
end;
hence thesis by Def5;
end;
hence thesis by A1,CLVECT_1:def 7;
end;
theorem
for X be non empty set for Y be ComplexNormSpace holds CLSStruct (#
ComplexBoundedFunctions(X,Y), Zero_(ComplexBoundedFunctions(X,Y),
ComplexVectSpace(X,Y)), Add_(ComplexBoundedFunctions(X,Y),ComplexVectSpace(X,Y)
), Mult_(ComplexBoundedFunctions(X,Y),ComplexVectSpace(X,Y)) #) is Subspace of
ComplexVectSpace(X,Y) by Th7,CSSPACE:11;
registration
let X be non empty set;
let Y be ComplexNormSpace;
cluster CLSStruct (# ComplexBoundedFunctions(X,Y), Zero_(
ComplexBoundedFunctions(X,Y), ComplexVectSpace(X,Y)), Add_(
ComplexBoundedFunctions(X,Y), ComplexVectSpace(X,Y)), Mult_(
ComplexBoundedFunctions(X,Y), ComplexVectSpace(X,Y)) #) -> Abelian
add-associative right_zeroed right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital;
coherence by Th7,CSSPACE:11;
end;
definition
let X be non empty set;
let Y be ComplexNormSpace;
func C_VectorSpace_of_BoundedFunctions(X,Y) -> ComplexLinearSpace equals
CLSStruct (# ComplexBoundedFunctions(X,Y), Zero_(ComplexBoundedFunctions(X,Y),
ComplexVectSpace(X,Y)), Add_(ComplexBoundedFunctions(X,Y),ComplexVectSpace(X,Y)
), Mult_(ComplexBoundedFunctions(X,Y),ComplexVectSpace(X,Y)) #);
coherence;
end;
registration
let X be non empty set;
let Y be ComplexNormSpace;
cluster C_VectorSpace_of_BoundedFunctions(X,Y) -> strict;
coherence;
end;
theorem Th9:
for X be non empty set for Y be ComplexNormSpace, f,g,h be
VECTOR of C_VectorSpace_of_BoundedFunctions(X,Y), 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 ComplexNormSpace;
let f,g,h be VECTOR of C_VectorSpace_of_BoundedFunctions(X,Y);
A1: C_VectorSpace_of_BoundedFunctions(X,Y) is Subspace of ComplexVectSpace(
X,Y) by Th7,CSSPACE:11;
then reconsider f1=f as VECTOR of ComplexVectSpace(X,Y) by CLVECT_1:29;
reconsider h1=h as VECTOR of ComplexVectSpace(X,Y) by A1,CLVECT_1:29;
reconsider g1=g as VECTOR of ComplexVectSpace(X,Y) by A1,CLVECT_1:29;
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,CLVECT_1:32;
hence h9.x=f9.x+g9.x by A2,CLOPBAN1:11;
end;
now
assume for x be Element of X holds h9.x=f9.x+g9.x;
then h1=f1+g1 by A2,CLOPBAN1:11;
hence h =f+g by A1,CLVECT_1:32;
end;
hence thesis by A3;
end;
theorem Th10:
for X be non empty set for Y be ComplexNormSpace, f,h be VECTOR
of C_VectorSpace_of_BoundedFunctions(X,Y), f9,h9 be bounded Function of X,the
carrier of Y st f9=f & h9=h for c be Complex holds h = c*f iff for x be Element
of X holds h9.x = c*f9.x
proof
let X be non empty set;
let Y be ComplexNormSpace;
let f,h be VECTOR of C_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 c be Complex;
A2: C_VectorSpace_of_BoundedFunctions(X,Y) is Subspace of ComplexVectSpace(
X,Y) by Th7,CSSPACE:11;
then reconsider f1=f, h1=h as VECTOR of ComplexVectSpace(X,Y) by CLVECT_1:29;
A3: now
assume
A4: h = c*f;
let x be Element of X;
h1=c*f1 by A2,A4,CLVECT_1:33;
hence h9.x=c*f9.x by A1,CLOPBAN1:12;
end;
now
assume for x be Element of X holds h9.x=c*f9.x;
then h1=c*f1 by A1,CLOPBAN1:12;
hence h =c*f by A2,CLVECT_1:33;
end;
hence thesis by A3;
end;
theorem Th11:
for X be non empty set, Y be ComplexNormSpace holds 0.
C_VectorSpace_of_BoundedFunctions(X,Y) = (X -->0.Y)
proof
let X be non empty set;
let Y be ComplexNormSpace;
C_VectorSpace_of_BoundedFunctions(X,Y) is Subspace of ComplexVectSpace(
X,Y) & 0.ComplexVectSpace(X,Y) = (X -->0.Y) by Th7,CSSPACE:11,LOPBAN_1:def 3;
hence thesis by CLVECT_1:30;
end;
definition
let X be non empty set;
let Y be ComplexNormSpace;
let f be object such that :: In(.,.) !!!
A1: f in ComplexBoundedFunctions(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 ComplexNormSpace;
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 Th12:
for X be non empty set for Y be ComplexNormSpace, 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 ComplexNormSpace;
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 ComplexNormSpace, 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 ComplexNormSpace;
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 by CLVECT_1:105;
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 Th12;
end;
definition
let X be non empty set;
let Y be ComplexNormSpace;
func ComplexBoundedFunctionsNorm(X,Y) -> Function of ComplexBoundedFunctions
(X,Y), REAL means
:Def9:
for x be object st x in ComplexBoundedFunctions(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 ComplexBoundedFunctions(X,Y) holds F(z) in REAL
by XREAL_0:def 1;
ex f being Function of ComplexBoundedFunctions(X,Y),REAL st
for x being object st x in ComplexBoundedFunctions(X,Y)
holds f.x = F(x) from FUNCT_2:sch 2(A1
);
hence thesis;
end;
uniqueness
proof
let NORM1,NORM2 be Function of ComplexBoundedFunctions(X,Y), REAL such
that
A2: for x be object st x in ComplexBoundedFunctions(X,Y) holds NORM1.x =
upper_bound PreNorms(modetrans(x,X,Y)) and
A3: for x be object st x in ComplexBoundedFunctions(X,Y) holds NORM2.x =
upper_bound PreNorms(modetrans(x,X,Y));
A4: for z be object st z in ComplexBoundedFunctions(X,Y)
holds NORM1.z = NORM2.z
proof
let z be object such that
A5: z in ComplexBoundedFunctions(X,Y);
NORM1.z = upper_bound PreNorms(modetrans(z,X,Y)) by A2,A5;
hence thesis by A3,A5;
end;
dom NORM1 = ComplexBoundedFunctions(X,Y) & dom NORM2 =
ComplexBoundedFunctions(X,Y) by FUNCT_2:def 1;
hence thesis by A4,FUNCT_1:2;
end;
end;
theorem Th14:
for X be non empty set, Y be ComplexNormSpace, 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 ComplexNormSpace;
let f be bounded Function of X,the carrier of Y;
f in ComplexBoundedFunctions(X,Y) by Def5;
hence thesis by Def7;
end;
theorem Th15:
for X be non empty set, Y be ComplexNormSpace, f be bounded
Function of X,the carrier of Y holds ComplexBoundedFunctionsNorm(X,Y).f
= upper_bound
PreNorms(f)
proof
let X be non empty set;
let Y be ComplexNormSpace;
let f be bounded Function of X,the carrier of Y;
reconsider f9=f as set;
f in ComplexBoundedFunctions(X,Y) by Def5;
hence
ComplexBoundedFunctionsNorm(X,Y).f = upper_bound PreNorms(modetrans(f9,X,Y))
by Def9
.= upper_bound PreNorms(f) by Th14;
end;
definition
let X be non empty set;
let Y be ComplexNormSpace;
func C_NormSpace_of_BoundedFunctions(X,Y) -> non empty CNORMSTR equals
CNORMSTR (# ComplexBoundedFunctions(X,Y), Zero_(ComplexBoundedFunctions(X,Y),
ComplexVectSpace(X,Y)), Add_(ComplexBoundedFunctions(X,Y),ComplexVectSpace(X,Y)
), Mult_(ComplexBoundedFunctions(X,Y),ComplexVectSpace(X,Y)),
ComplexBoundedFunctionsNorm(X,Y) #);
coherence;
end;
theorem Th16:
for X be non empty set, Y be ComplexNormSpace holds (X --> 0.Y)
= 0.C_NormSpace_of_BoundedFunctions(X,Y)
proof
let X be non empty set;
let Y be ComplexNormSpace;
(X --> 0.Y) =0.C_VectorSpace_of_BoundedFunctions(X,Y) by Th11
.=0.C_NormSpace_of_BoundedFunctions(X,Y);
hence thesis;
end;
theorem Th17:
for X be non empty set, Y be ComplexNormSpace, f being Point of
C_NormSpace_of_BoundedFunctions(X,Y), 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 ComplexNormSpace;
let f being Point of C_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 Th12;
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;
then ||.g.t.|| <= ComplexBoundedFunctionsNorm(X,Y).g by Th15;
hence ||.g.t.|| <= ||.f.|| by A1;
end;
hence thesis;
end;
theorem
for X be non empty set, Y be ComplexNormSpace, f being Point of
C_NormSpace_of_BoundedFunctions(X,Y) holds 0 <= ||.f.||
proof
let X be non empty set;
let Y be ComplexNormSpace;
let f being Point of C_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 Th12;
A3: ComplexBoundedFunctionsNorm(X,Y).f = upper_bound PreNorms(g) by Th15;
now
let r be Real;
assume r in PreNorms(g);
then ex t be Element of X st r=||.g.t.||;
hence 0 <= r by CLVECT_1:105;
end;
then 0 <= r0 by A1;
then 0 <=upper_bound PreNorms(g) by A2,A1,SEQ_4:def 1;
hence thesis by A3;
end;
theorem Th19:
for X be non empty set, Y be ComplexNormSpace, f being Point of
C_NormSpace_of_BoundedFunctions(X,Y) st f = 0.C_NormSpace_of_BoundedFunctions(X
,Y) holds 0 = ||.f.||
proof
let X be non empty set;
let Y be ComplexNormSpace;
let f being Point of C_NormSpace_of_BoundedFunctions(X,Y) such that
A1: f = 0.C_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 Th12;
A5: z=g by A1,Th16;
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;
then ComplexBoundedFunctionsNorm(X,Y).f=0 by Th15;
hence thesis;
end;
end;
theorem Th20:
for X be non empty set, Y be ComplexNormSpace, f,g,h be Point of
C_NormSpace_of_BoundedFunctions(X,Y), 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 ComplexNormSpace;
let f,g,h be Point of C_NormSpace_of_BoundedFunctions(X,Y);
reconsider f1=f, g1=g, h1=h as VECTOR of C_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,Th9;
end;
theorem Th21:
for X be non empty set, Y be ComplexNormSpace, f,h be Point of
C_NormSpace_of_BoundedFunctions(X,Y), f9,h9 be bounded Function of X,the
carrier of Y st f9=f & h9=h for c be Complex holds h = c*f iff for x be Element
of X holds h9.x = c*f9.x
proof
let X be non empty set;
let Y be ComplexNormSpace;
let f,h be Point of C_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 C_VectorSpace_of_BoundedFunctions(X,Y);
reconsider f1=f as VECTOR of C_VectorSpace_of_BoundedFunctions(X,Y);
let c be Complex;
A2: now
assume h1=c*f1;
hence h=Mult_(ComplexBoundedFunctions(X,Y), ComplexVectSpace(X,Y)) .[c,f1]
by CLVECT_1:def 1
.=c*f by CLVECT_1:def 1;
end;
now
assume h=c*f;
hence h1=Mult_(ComplexBoundedFunctions(X,Y), ComplexVectSpace(X,Y)).[c,f]
by CLVECT_1:def 1
.=c*f1 by CLVECT_1:def 1;
end;
hence thesis by A1,A2,Th10;
end;
theorem Th22:
for X be non empty set, Y be ComplexNormSpace, f,g being Point
of C_NormSpace_of_BoundedFunctions(X,Y), c be Complex holds ( ||.f.|| = 0 iff f
= 0.C_NormSpace_of_BoundedFunctions(X,Y) ) & ||.c*f.|| = |.c.| * ||.f.|| & ||.f
+g.|| <= ||.f.|| + ||.g.||
proof
let X be non empty set;
let Y be ComplexNormSpace;
let f, g being Point of C_NormSpace_of_BoundedFunctions(X,Y);
let c be Complex;
A1: now
assume
A2: f = 0.C_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 Th12;
A6: z=g by A2,Th16;
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;
then ComplexBoundedFunctionsNorm(X,Y).f =0 by Th15;
hence thesis;
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: (for s be Real st s in PreNorms(h1) holds s <= ||.f.|| + ||.g
.||) implies upper_bound PreNorms(h1) <= ||.f.|| + ||.g.|| by SEQ_4:45;
A11: now
let t be Element of X;
||.f1.t.||<= ||.f.|| & ||.g1.t.||<= ||.g.|| by Th17;
then
A12: ||.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 Th20,CLVECT_1:def 13;
hence ||.h1.t.|| <= ||.f.|| + ||.g.|| by A12,XXREAL_0:2;
end;
A13: 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 A11;
end;
ComplexBoundedFunctionsNorm(X,Y).(f+g) = upper_bound PreNorms(h1) by Th15;
hence thesis by A13,A10;
end;
A14: ||.c*f.|| = |.c.| * ||.f.||
proof
reconsider f1=f, h1=c*f as bounded Function of X, the carrier of Y by Def5;
A15: (for s be Real st s in PreNorms(h1) holds s <= |.c.|*||.f.|| )
implies upper_bound PreNorms(h1) <= |.c.|*||.f.|| by SEQ_4:45;
A16: now
let t be Element of X;
A17: 0<= |.c.| by COMPLEX1:46;
||.h1.t.||= ||.c*f1.t.|| & ||.c*f1.t.|| =|.c.|*||.f1.t.|| by Th21,
CLVECT_1:def 13;
hence ||.h1.t.|| <= |.c.|*||.f.|| by A17,Th17,XREAL_1:64;
end;
A18: now
let r be Real;
assume r in PreNorms(h1);
then ex t be Element of X st r=||.h1.t.||;
hence r <= |.c.|*||.f.|| by A16;
end;
A19: now
per cases;
case
A20: c <> 0c;
A21: now
let t be Element of X;
A22: |.c".| = |.1r/c.| by COMPLEX1:def 4,XCMPLX_1:215
.= 1/|.c.| by COMPLEX1:48,67
.= 1*(|.c.|)" by XCMPLX_0:def 9
.= |.c.|";
h1.t=c*f1.t by Th21;
then
A23: c"*h1.t =( c"* c)*f1.t by CLVECT_1:def 4
.=1r*f1.t by A20,COMPLEX1:def 4,XCMPLX_0:def 7
.=f1.t by CLVECT_1:def 5;
||.c"*h1.t.|| =|.c".|*||.h1.t.|| & 0<= |.c".| by CLVECT_1:def 13
,COMPLEX1:46;
hence ||.f1.t.|| <= |.c.|"*||.c*f.|| by A23,A22,Th17,XREAL_1:64;
end;
A24: now
let r be Real;
assume r in PreNorms(f1);
then ex t be Element of X st r=||.f1.t.||;
hence r <= |.c.|"*||.c*f.|| by A21;
end;
A25: ( for s be Real st s in PreNorms(f1) holds s <= |.c.|"*||.
c*f.|| ) implies upper_bound PreNorms(f1) <= |.c.|"*||.c*f.||
by SEQ_4:45;
A26: 0 <= |.c.| by COMPLEX1:46;
ComplexBoundedFunctionsNorm(X,Y).(f) = upper_bound PreNorms(f1)
by Th15;
then ||.f.|| <=|.c.|"*||.c*f.|| by A24,A25;
then |.c.|*||.f.|| <= |.c.|*(|.c.|"*||.c*f.||) by A26,XREAL_1:64;
then
A27: |.c.|*||.f.|| <=(|.c.|*|.c.|")*||.c*f.||;
|.c.| <>0 by A20,COMPLEX1:47;
then |.c.|*||.f.|| <=1*||.c*f.|| by A27,XCMPLX_0:def 7;
hence |.c.|* ||.f.|| <=||.c*f.||;
end;
case
A28: c = 0c;
reconsider fz=f as VECTOR of C_VectorSpace_of_BoundedFunctions(X,Y);
c*f =Mult_(ComplexBoundedFunctions(X,Y), ComplexVectSpace(X,Y)).[
c,f] by CLVECT_1:def 1
.=c*fz by CLVECT_1:def 1
.=0.C_VectorSpace_of_BoundedFunctions(X,Y) by A28,CLVECT_1:1
.=0.C_NormSpace_of_BoundedFunctions(X,Y);
hence thesis by A28,Th19,COMPLEX1:44;
end;
end;
ComplexBoundedFunctionsNorm(X,Y).(c*f) = upper_bound PreNorms(h1) by Th15;
then ||.c*f.|| <= |.c.|*||.f.|| by A18,A15;
hence thesis by A19,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
A29: ||.f.|| = 0;
now
let t be Element of X;
||.g.t.|| <= ||.f.|| by Th17;
then ||.g.t.|| = 0 by A29,CLVECT_1:105;
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.C_NormSpace_of_BoundedFunctions(X,Y) by Th16;
end;
hence thesis by A1,A14,A9;
end;
theorem Th23:
for X be non empty set, Y be ComplexNormSpace holds
C_NormSpace_of_BoundedFunctions(X,Y) is
reflexive discerning ComplexNormSpace-like
proof
let X be non empty set;
let Y be ComplexNormSpace;
thus ||.0.C_NormSpace_of_BoundedFunctions(X,Y).|| = 0 by Th22;
for x, y being Point of C_NormSpace_of_BoundedFunctions(X,Y) for c be
Complex holds ( ||.x.|| = 0 iff x = 0.C_NormSpace_of_BoundedFunctions(X,Y) ) &
||.c*x.|| = |.c.| * ||.x.|| & ||.x+y.|| <= ||.x.|| + ||.y.|| by Th22;
hence thesis by CLVECT_1:def 13;
end;
theorem Th24:
for X be non empty set, Y be ComplexNormSpace holds
C_NormSpace_of_BoundedFunctions(X,Y) is ComplexNormSpace
proof
let X be non empty set;
let Y be ComplexNormSpace;
CLSStruct (# ComplexBoundedFunctions(X,Y), Zero_(ComplexBoundedFunctions
(X,Y),ComplexVectSpace(X,Y)), Add_(ComplexBoundedFunctions(X,Y),
ComplexVectSpace(X,Y)), Mult_(ComplexBoundedFunctions(X,Y),ComplexVectSpace(X,Y
)) #) is ComplexLinearSpace;
hence thesis by Th23,CSSPACE3:2;
end;
registration
let X be non empty set;
let Y be ComplexNormSpace;
cluster C_NormSpace_of_BoundedFunctions(X,Y) ->
reflexive discerning ComplexNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed
right_complementable;
coherence by Th24;
end;
theorem Th25:
for X be non empty set for Y be ComplexNormSpace, f,g,h be Point
of C_NormSpace_of_BoundedFunctions(X,Y), 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 ComplexNormSpace;
let f,g,h be Point of C_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 by RLVECT_1:13;
end;
then f=h+g by A1,Th20;
then f-g=h+(g-g) by RLVECT_1:def 3;
then f-g=h+0.C_NormSpace_of_BoundedFunctions(X,Y) by RLVECT_1:15;
hence f-g=h by RLVECT_1:4;
end;
now
assume h=f-g;
then h+g=f-(g-g) by RLVECT_1:29;
then h+g=f-0.C_NormSpace_of_BoundedFunctions(X,Y) by RLVECT_1:15;
then
A4: h+g=f by RLVECT_1:13;
now
let x be Element of X;
f9.x=h9.x + g9.x by A1,A4,Th20;
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 by RLVECT_1:4;
end;
hence for x be Element of X holds h9.x = f9.x - g9.x;
end;
hence thesis by A2;
end;
Lm12: 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;
(seq ^\k).i = seq.(k+i) & 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 Th26:
for X be non empty set, Y be ComplexNormSpace st Y is complete
for seq be sequence of C_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 ComplexNormSpace such that
A1: Y is complete;
let vseq be sequence of C_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;
A7: k in NAT & m in NAT by ORDINAL1:def 12;
vseq.k is bounded Function of X,the carrier of Y by Def5;
then
A8: modetrans((vseq.k),X,Y)=vseq.k by Th14;
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
A9: modetrans((vseq.m),X,Y)=vseq.m by Th14;
xseq.m = modetrans((vseq.m),X,Y).x & xseq.k = modetrans((vseq.k),X,
Y).x by A4,A7;
then xseq.m - xseq.k = h1.x by A9,A8,Th25;
hence thesis by Th17;
end;
now
let e be Real such that
A10: 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
A11: for n, m be Nat st n >= k & m >= k holds ||.(vseq.
n) - (vseq.m).|| < e by A2,A10,CSSPACE3: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
A12: ||.(vseq.n) - (vseq.m).|| < e by A11;
||.xseq.n-xseq.m.|| <= ||.(vseq.n) - (vseq.m).|| by A6;
hence thesis by A12,XXREAL_0:2;
end;
end;
end;
then xseq is Cauchy_sequence_by_Norm by CSSPACE3:8;
then xseq is convergent by A1;
hence thesis by A5;
end;
consider f be Function of X,the carrier of Y such that
A13: 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
A14: e1 >0;
reconsider e =e1 as Real;
consider k be Nat such that
A15: for n, m be Nat st n >= k & m >= k holds ||.(vseq.n) -
(vseq.m).|| < e by A2,A14,CSSPACE3:8;
take k;
now
let m be Nat;
assume m >= k;
then
A16: ||.vseq.m.||= ||.vseq.||.m & ||.(vseq.m) - (vseq.k).|| <e by A15,
NORMSP_0:def 4;
|. ||.vseq.m.||- ||.vseq.k.|| .| <= ||.(vseq.m) - (vseq.k).|| & ||.
vseq.k .||= ||.vseq.||.k by CLVECT_1:110,NORMSP_0:def 4;
hence |. ||.vseq.||.m - ||.vseq.||.k .| <e1 by A16,XXREAL_0:2;
end;
hence
for m be Nat st m >= k holds |.||.vseq.||.m - ||.vseq.||
.k .| < e1;
end;
then
A17: ||.vseq.|| is convergent by SEQ_4:41;
A18: tseq is bounded
proof
take lim (||.vseq.|| );
A19: now
let x be Element of X;
consider xseq be sequence of Y such that
A20: for n be Nat holds xseq.n=modetrans((vseq.n),X,Y).x and
A21: xseq is convergent & tseq.x = lim xseq by A13;
A22: 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 A20,Def5;
hence thesis by Th14,Th17;
end;
A23: for n be Nat holds ||.xseq.||.n <=(||.vseq.||).n
proof
let n be Nat;
||.xseq.||.n = ||.(xseq.n).|| & ||.(xseq.n).|| <= ||.vseq.n.|| by A22,
NORMSP_0:def 4;
hence thesis by NORMSP_0:def 4;
end;
||.xseq.|| is convergent & ||.tseq.x.|| = lim ||.xseq.|| by A21,
CLOPBAN1:40;
hence ||.tseq.x.|| <= lim (||.vseq.|| ) by A17,A23,SEQ_2:18;
end;
now
let n be Nat;
||.vseq.n.|| >=0 by CLVECT_1:105;
hence ||.vseq.||.n >=0 by NORMSP_0:def 4;
end;
hence thesis by A17,A19,SEQ_2:17;
end;
A24: for e be Real st e > 0 ex k be Nat st
for n be Nat st n >= k
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
A25: for n, m be Nat st n >= k & m >= k holds ||.(vseq.n) -
(vseq.m).|| < e by A2,CSSPACE3:8;
take k;
now
let n be Nat such that
A26: n >= k;
now
let x be Element of X;
consider xseq be sequence of Y such that
A27: for n be Nat holds xseq.n=modetrans((vseq.n),X,Y). x and
A28: xseq is convergent & tseq.x = lim xseq by A13;
A29: 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
A30: modetrans((vseq.k),X,Y)=vseq.k by Th14;
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
A31: modetrans((vseq.m),X,Y)=vseq.m by Th14;
xseq.m =modetrans((vseq.m),X,Y).x & xseq.k =modetrans((vseq.k),
X,Y).x by A27;
then xseq.m - xseq.k =h1.x by A31,A30,Th25;
hence thesis by Th17;
end;
A32: for m be Nat st m >=k holds ||.xseq.n-xseq.m.|| <= e
proof
let m be Nat;
assume m >=k;
then
A33: ||.vseq.n - vseq.m.|| <e by A25,A26;
||.xseq.n-xseq.m.|| <= ||.vseq.n - vseq.m.|| by A29;
hence thesis by A33,XXREAL_0:2;
end;
||.xseq.n-tseq.x.|| <= e
proof
deffunc F(Nat) = ||.xseq.$1 - xseq.n.||;
consider rseq be Real_Sequence such that
A34: 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 A34
.= ||.(xseq - xseq.n).k.|| by NORMSP_1:def 4
.= ||.(xseq - xseq.n).||.x by NORMSP_0:def 4;
end;
then
A35: rseq = ||.xseq - xseq.n.|| by FUNCT_2:12;
A36: xseq - xseq.n is convergent & lim (xseq-xseq.n)= tseq.x - xseq.
n by A28,CLVECT_1:115,121;
then
A37: lim rseq = ||.tseq.x-xseq.n.|| by A35,CLOPBAN1:19;
for m be Nat st m >= k holds rseq.m <= e
proof
let m be Nat such that
A38: m >=k;
rseq.m = ||.xseq.m-xseq.n.|| by A34
.= ||.xseq.n-xseq.m.|| by CLVECT_1:108;
hence thesis by A32,A38;
end;
then lim rseq <= e by A36,A35,Lm12,CLOPBAN1:19;
hence thesis by A37,CLVECT_1:108;
end;
hence ||.modetrans((vseq.n),X,Y).x - tseq.x.|| <= e by A27;
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 A18;
reconsider tv=tseq as Point of C_NormSpace_of_BoundedFunctions(X,Y) by Def5;
A39: 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
A40: 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 A24;
now
set g1=tseq;
let n be Nat such that
A41: 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);
A42: 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 Th14;
then ||.h1.t.||= ||.f1.t-g1.t.|| by Th25;
hence ||.h1.t.|| <=e by A40,A41;
end;
A43: 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 A42;
end;
A44: (for s be Real st s in PreNorms(h1) holds s <= e) implies
upper_bound PreNorms(h1) <=e by SEQ_4:45;
ComplexBoundedFunctionsNorm(X,Y).(vseq.n-tv) = upper_bound PreNorms(h1)
by Th15;
hence ||.vseq.n-tv.|| <=e by A43,A44;
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
A45: e > 0;
reconsider ee=e as Real;
consider m be Nat such that
A46: for n be Nat st n >= m holds ||.(vseq.n) - tv.|| <= ee/
2 by A39,A45;
A47: e/2<e by A45,XREAL_1:216;
now
let n be Nat;
assume n >= m;
then ||.(vseq.n) - tv.|| <= e/2 by A46;
hence ||.(vseq.n) - tv.|| < e by A47,XXREAL_0:2;
end;
hence thesis;
end;
hence thesis by CLVECT_1:def 15;
end;
theorem Th27:
for X be non empty set, Y be ComplexBanachSpace holds
C_NormSpace_of_BoundedFunctions(X,Y) is ComplexBanachSpace
proof
let X be non empty set;
let Y be ComplexBanachSpace;
for seq be sequence of C_NormSpace_of_BoundedFunctions(X,Y) st seq is
Cauchy_sequence_by_Norm holds seq is convergent by Th26;
hence thesis by CLOPBAN1:def 13;
end;
registration
let X be non empty set;
let Y be ComplexBanachSpace;
cluster C_NormSpace_of_BoundedFunctions (X,Y) -> complete;
coherence by Th27;
end;
begin :: Some properties of complex sequences
theorem
for seq1,seq2 be Complex_Sequence st seq1 is bounded & seq2 is bounded
holds seq1 + seq2 is bounded by Lm3;
theorem
for c be Complex, seq be Complex_Sequence st seq is bounded holds c(#)
seq is bounded by Lm4;
theorem
for seq be Complex_Sequence holds seq is bounded iff |.seq.| is
bounded by Lm8,Lm9;
theorem
for seq1,seq2,seq3 be Complex_Sequence holds seq1 = seq2 - seq3 iff
for n be Nat holds seq1.n = seq2.n - seq3.n by Lm11;