:: Complex Banach Space of Bounded Complex Sequences :: by Noboru Endou :: :: Received March 18, 2004 :: Copyright (c) 2004-2021 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; begin definition func the_set_of_BoundedComplexSequences -> Subset of Linear_Space_of_ComplexSequences means :: CSSPACE4:def 1 for x being object holds x in it iff x in the_set_of_ComplexSequences & seq_id x is bounded; end; registration cluster the_set_of_BoundedComplexSequences -> non empty; cluster the_set_of_BoundedComplexSequences -> linearly-closed; end; 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; end; definition func Complex_linfty_norm -> Function of the_set_of_BoundedComplexSequences, REAL means :: CSSPACE4:def 2 for x be object st x in the_set_of_BoundedComplexSequences holds it.x = upper_bound rng |.seq_id x.|; end; theorem :: CSSPACE4:1 for seq be Complex_Sequence holds seq is bounded & upper_bound rng |.seq.| = 0 iff for n be Nat holds seq.n = 0c; 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; end; definition func Complex_linfty_Space -> non empty CNORMSTR equals :: CSSPACE4:def 3 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 #); end; theorem :: CSSPACE4:2 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.|; theorem :: CSSPACE4:3 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.||; registration cluster Complex_linfty_Space -> reflexive discerning ComplexNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable; end; theorem :: CSSPACE4:4 for vseq be sequence of Complex_linfty_Space st vseq is Cauchy_sequence_by_Norm holds vseq is convergent; theorem :: CSSPACE4:5 Complex_linfty_Space is ComplexBanachSpace; 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 :: CSSPACE4:def 4 ex K being Real st 0 <= K & for x being Element of X holds ||. IT.x .|| <= K; end; theorem :: CSSPACE4:6 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 ; registration let X be non empty set; let Y be ComplexNormSpace; cluster bounded for Function of X,the carrier of Y; end; definition let X be non empty set; let Y be ComplexNormSpace; func ComplexBoundedFunctions(X,Y) -> Subset of ComplexVectSpace(X,Y) means :: CSSPACE4:def 5 for x being set holds x in it iff x is bounded Function of X,the carrier of Y; end; registration let X be non empty set; let Y be ComplexNormSpace; cluster ComplexBoundedFunctions(X,Y) -> non empty; end; theorem :: CSSPACE4:7 for X be non empty set for Y be ComplexNormSpace holds ComplexBoundedFunctions(X,Y) is linearly-closed; theorem :: CSSPACE4:8 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); 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; end; definition let X be non empty set; let Y be ComplexNormSpace; func C_VectorSpace_of_BoundedFunctions(X,Y) -> ComplexLinearSpace equals :: CSSPACE4:def 6 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)) #); end; registration let X be non empty set; let Y be ComplexNormSpace; cluster C_VectorSpace_of_BoundedFunctions(X,Y) -> strict; end; theorem :: CSSPACE4:9 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 ); theorem :: CSSPACE4:10 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; theorem :: CSSPACE4:11 for X be non empty set, Y be ComplexNormSpace holds 0. C_VectorSpace_of_BoundedFunctions(X,Y) = (X -->0.Y); definition let X be non empty set; let Y be ComplexNormSpace; let f be object such that :: In(.,.) !!! f in ComplexBoundedFunctions(X,Y); func modetrans(f,X,Y) -> bounded Function of X,the carrier of Y equals :: CSSPACE4:def 7 f; 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 :: CSSPACE4:def 8 the set of all ||.u.t.|| where t is Element of X ; end; theorem :: CSSPACE4:12 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; theorem :: CSSPACE4:13 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; definition let X be non empty set; let Y be ComplexNormSpace; func ComplexBoundedFunctionsNorm(X,Y) -> Function of ComplexBoundedFunctions (X,Y), REAL means :: CSSPACE4:def 9 for x be object st x in ComplexBoundedFunctions(X,Y) holds it.x = upper_bound PreNorms(modetrans(x,X,Y)); end; theorem :: CSSPACE4:14 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; theorem :: CSSPACE4:15 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); definition let X be non empty set; let Y be ComplexNormSpace; func C_NormSpace_of_BoundedFunctions(X,Y) -> non empty CNORMSTR equals :: CSSPACE4:def 10 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) #); end; theorem :: CSSPACE4:16 for X be non empty set, Y be ComplexNormSpace holds (X --> 0.Y) = 0.C_NormSpace_of_BoundedFunctions(X,Y); theorem :: CSSPACE4:17 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.||; theorem :: CSSPACE4:18 for X be non empty set, Y be ComplexNormSpace, f being Point of C_NormSpace_of_BoundedFunctions(X,Y) holds 0 <= ||.f.||; theorem :: CSSPACE4:19 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.||; theorem :: CSSPACE4:20 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 ); theorem :: CSSPACE4:21 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; theorem :: CSSPACE4:22 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.||; theorem :: CSSPACE4:23 for X be non empty set, Y be ComplexNormSpace holds C_NormSpace_of_BoundedFunctions(X,Y) is reflexive discerning ComplexNormSpace-like; theorem :: CSSPACE4:24 for X be non empty set, Y be ComplexNormSpace holds C_NormSpace_of_BoundedFunctions(X,Y) is ComplexNormSpace; 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; end; theorem :: CSSPACE4:25 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 ); theorem :: CSSPACE4:26 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; theorem :: CSSPACE4:27 for X be non empty set, Y be ComplexBanachSpace holds C_NormSpace_of_BoundedFunctions(X,Y) is ComplexBanachSpace; registration let X be non empty set; let Y be ComplexBanachSpace; cluster C_NormSpace_of_BoundedFunctions (X,Y) -> complete; end; begin :: Some properties of complex sequences theorem :: CSSPACE4:28 for seq1,seq2 be Complex_Sequence st seq1 is bounded & seq2 is bounded holds seq1 + seq2 is bounded; theorem :: CSSPACE4:29 for c be Complex, seq be Complex_Sequence st seq is bounded holds c(#) seq is bounded; theorem :: CSSPACE4:30 for seq be Complex_Sequence holds seq is bounded iff |.seq.| is bounded; theorem :: CSSPACE4:31 for seq1,seq2,seq3 be Complex_Sequence holds seq1 = seq2 - seq3 iff for n be Nat holds seq1.n = seq2.n - seq3.n;