:: Complex Linear Space of Complex Sequences :: by Noboru Endou :: :: Received January 26, 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, XBOOLE_0, COMSEQ_1, FUNCT_2, TARSKI, RSSPACE, BINOP_1, SUBSET_1, FUNCT_1, ARYTM_3, ZFMISC_1, VALUED_1, COMPLEX1, FUNCOP_1, RLVECT_1, CLVECT_1, RELAT_1, SUPINF_2, ARYTM_1, STRUCT_0, ALGSTR_0, RLSUB_1, REALSET1, SERIES_1, CARD_1, XXREAL_0, REAL_1, SQUARE_1, BHSP_1, PRE_TOPC, PROB_2, XCMPLX_0, RVSUM_1, NORMSP_1, METRIC_1, NAT_1, CARD_3, SEQ_2, ORDINAL2, CSSPACE, CLOPBAN1, CFUNCDOM; notations TARSKI, XBOOLE_0, SUBSET_1, PRE_TOPC, RELAT_1, DOMAIN_1, FUNCT_1, FUNCT_2, FUNCOP_1, VALUED_1, BINOP_1, REALSET1, XCMPLX_0, XXREAL_0, REAL_1, ORDINAL1, NAT_1, STRUCT_0, ALGSTR_0, ZFMISC_1, NUMBERS, SQUARE_1, XREAL_0, COMPLEX1, COMSEQ_1, COMSEQ_2, SERIES_1, COMSEQ_3, RLVECT_1, VFUNCT_1, NORMSP_1, BHSP_1, CLVECT_1, CFUNCDOM; constructors BINOP_1, FUNCOP_1, REAL_1, SQUARE_1, COMSEQ_2, COMSEQ_3, REALSET1, BHSP_1, CLVECT_1, RELSET_1, VFUNCT_1, CFUNCDOM, FUNCSDOM; registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, MEMBERED, REALSET1, STRUCT_0, CLVECT_1, ALGSTR_0, VALUED_1, VALUED_0, VFUNCT_1, SERIES_1, XREAL_0, SQUARE_1, CFUNCDOM; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; begin definition func the_set_of_ComplexSequences -> non empty set equals :: CSSPACE:def 1 Funcs(NAT,COMPLEX); end; definition let z be object such that z in the_set_of_ComplexSequences; func seq_id(z) -> Complex_Sequence equals :: CSSPACE:def 2 z; end; registration let z be Element of the_set_of_ComplexSequences; reduce seq_id(z) to z; end; definition let z be object such that z is Complex; func C_id(z) -> Complex equals :: CSSPACE:def 3 z; end; registration let z be Complex; reduce C_id(z) to z; end; definition ::$CD 2 func CZeroseq -> Element of the_set_of_ComplexSequences equals :: CSSPACE:def 6 NAT --> 0c; end; registration let x be Complex_Sequence; reduce seq_id x to x; end; theorem :: CSSPACE:1 for x being Complex_Sequence holds seq_id x = x; definition func Linear_Space_of_ComplexSequences -> strict non empty CLSStruct equals :: CSSPACE:def 7 ComplexVectSpace(NAT); end; registration cluster Linear_Space_of_ComplexSequences -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital; end; registration let z be VECTOR of Linear_Space_of_ComplexSequences; reduce seq_id(z) to z; end; theorem :: CSSPACE:2 for v,w being VECTOR of Linear_Space_of_ComplexSequences holds v + w = seq_id(v) + seq_id(w); theorem :: CSSPACE:3 for z being Complex, v being VECTOR of Linear_Space_of_ComplexSequences holds z * v = z(#)seq_id(v); theorem :: CSSPACE:4 for n being object holds (seq_id CZeroseq).n = 0; theorem :: CSSPACE:5 for f being Element of the_set_of_ComplexSequences st for n being Nat holds (seq_id f).n = 0 holds f = CZeroseq; ::$CT 5 definition let X be ComplexLinearSpace; let X1 be Subset of X such that X1 is linearly-closed; func Add_(X1,X) -> BinOp of X1 equals :: CSSPACE:def 8 (the addF of X) || X1; end; definition let X be ComplexLinearSpace; let X1 be Subset of X such that X1 is linearly-closed; func Mult_(X1,X) -> Function of [:COMPLEX,X1:], X1 equals :: CSSPACE:def 9 (the Mult of X) | [:COMPLEX,X1:]; end; definition let X be ComplexLinearSpace, X1 be Subset of X such that X1 is linearly-closed and X1 is non empty; func Zero_(X1,X) -> Element of X1 equals :: CSSPACE:def 10 0.X; end; theorem :: CSSPACE:11 for V be ComplexLinearSpace, V1 be Subset of V st V1 is linearly-closed non empty holds CLSStruct (# V1,Zero_(V1,V), Add_(V1,V), Mult_(V1,V) #) is Subspace of V; definition func the_set_of_l2ComplexSequences -> Subset of Linear_Space_of_ComplexSequences means :: CSSPACE:def 11 for x being object holds x in it iff x in the_set_of_ComplexSequences & |.seq_id(x).| (#) |.seq_id(x).| is summable; end; registration cluster the_set_of_l2ComplexSequences -> non empty; end; theorem :: CSSPACE:12 the_set_of_l2ComplexSequences is linearly-closed; registration cluster the_set_of_l2ComplexSequences -> linearly-closed; end; registration let z be Element of the_set_of_l2ComplexSequences; reduce seq_id(z) to z; end; theorem :: CSSPACE:13 CLSStruct(# the_set_of_l2ComplexSequences, Zero_( the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences), Add_( the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences), Mult_( the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences) #) is Subspace of Linear_Space_of_ComplexSequences; theorem :: CSSPACE:14 CLSStruct (# the_set_of_l2ComplexSequences, Zero_( the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences), Add_( the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences), Mult_( the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences) #) is ComplexLinearSpace; theorem :: CSSPACE:15 the carrier of Linear_Space_of_ComplexSequences = the_set_of_ComplexSequences & (for x be set holds x is VECTOR of Linear_Space_of_ComplexSequences iff x is Complex_Sequence) & (for u be VECTOR of Linear_Space_of_ComplexSequences holds u =seq_id(u)) & (for u,v be VECTOR of Linear_Space_of_ComplexSequences holds u+v =seq_id(u)+seq_id(v)) & for z be Complex for u be VECTOR of Linear_Space_of_ComplexSequences holds z*u =z(#)seq_id(u); begin :: Unitary space with complex coefficient definition struct(CLSStruct) CUNITSTR (# carrier -> set, ZeroF -> Element of the carrier, addF -> BinOp of the carrier, Mult -> Function of [:COMPLEX, the carrier:], the carrier, scalar -> Function of [: the carrier, the carrier :], COMPLEX #); end; registration cluster non empty strict for CUNITSTR; end; registration let D be non empty set, Z be Element of D, a be BinOp of D,m be Function of [:COMPLEX, D:], D, s be Function of [: D,D:],COMPLEX; cluster CUNITSTR (#D,Z,a,m,s#) -> non empty; end; reserve X for non empty CUNITSTR; reserve a, b for Complex; reserve x, y for Point of X; definition let X; let x, y; func x .|. y -> Complex equals :: CSSPACE:def 12 (the scalar of X).(x,y); end; definition let IT be non empty CUNITSTR; attr IT is ComplexUnitarySpace-like means :: CSSPACE:def 13 for x,y,w being Point of IT, a holds ( x .|. x = 0 iff x = 0.IT ) & 0 <= Re(x .|. x) & 0 = Im(x .|. x) & x .|. y = (y .|. x)*' & (x+y) .|. w = x .|. w + y .|. w & (a*x) .|. y = a * ( x .|. y ); end; registration cluster ComplexUnitarySpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable strict for non empty CUNITSTR; end; definition mode ComplexUnitarySpace is ComplexUnitarySpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable non empty CUNITSTR; end; reserve X for ComplexUnitarySpace; reserve x, y, z, u, v for Point of X; theorem :: CSSPACE:16 (0.X).|.(0.X) = 0; theorem :: CSSPACE:17 x.|.(y+z) = x.|.y + x.|.z; theorem :: CSSPACE:18 x.|.(a*y) = (a*') * x.|.y; theorem :: CSSPACE:19 (a*x).|.y = x.|.((a*')*y); theorem :: CSSPACE:20 (a*x + b*y).|.z = a * x.|.z + b * y.|.z; theorem :: CSSPACE:21 x.|.(a*y + b*z) = (a*') * x.|.y + (b*') * x.|.z; theorem :: CSSPACE:22 (-x) .|. y = x .|. (-y); theorem :: CSSPACE:23 (-x).|.y = - x.|.y; theorem :: CSSPACE:24 x.|.(-y) = - x.|.y; theorem :: CSSPACE:25 (-x).|.(-y) = x.|.y; theorem :: CSSPACE:26 (x-y).|.z = x.|.z - y.|.z; theorem :: CSSPACE:27 x.|.(y-z) = x.|.y - x.|.z; theorem :: CSSPACE:28 (x-y).|.(u-v) = x.|.u - x.|.v - y.|.u + y.|.v; theorem :: CSSPACE:29 (0.X).|.x = 0; theorem :: CSSPACE:30 x.|.0.X = 0; theorem :: CSSPACE:31 (x+y).|.(x+y) = x.|.x + x.|.y + y.|.x + y.|.y; theorem :: CSSPACE:32 (x+y).|.(x-y) = x.|.x - x.|.y + y.|.x - y.|.y; theorem :: CSSPACE:33 (x-y).|.(x-y) = x.|.x - x.|.y - y.|.x + y.|.y; theorem :: CSSPACE:34 |.(x.|.x).| = Re(x.|.x); theorem :: CSSPACE:35 ::Schwarz's inequality |.(x.|.y).| <= sqrt|.(x.|.x).| * sqrt|.(y.|.y).|; definition let X; let x, y; pred x, y are_orthogonal means :: CSSPACE:def 14 x .|. y = 0; symmetry; end; theorem :: CSSPACE:36 x, y are_orthogonal implies x, - y are_orthogonal; theorem :: CSSPACE:37 x, y are_orthogonal implies -x, y are_orthogonal; theorem :: CSSPACE:38 x, y are_orthogonal implies -x, -y are_orthogonal; theorem :: CSSPACE:39 x, 0.X are_orthogonal; theorem :: CSSPACE:40 x,y are_orthogonal implies (x+y).|.(x+y) = x.|.x + y.|.y; theorem :: CSSPACE:41 x,y are_orthogonal implies (x-y).|.(x-y) = x.|.x + y.|.y; definition let X, x; func ||.x.|| -> Real equals :: CSSPACE:def 15 sqrt |.(x.|.x).|; end; theorem :: CSSPACE:42 ||.x.|| = 0 iff x = 0.X; theorem :: CSSPACE:43 ||.a * x.|| = |.a.| * ||.x.||; theorem :: CSSPACE:44 0 <= ||.x.||; theorem :: CSSPACE:45 |.(x.|.y).| <= ||.x.|| * ||.y.||; theorem :: CSSPACE:46 ||.x + y.|| <= ||.x.|| + ||.y.||; theorem :: CSSPACE:47 ||.-x.|| = ||.x.||; theorem :: CSSPACE:48 ||.x.|| - ||.y.|| <= ||.x - y.||; theorem :: CSSPACE:49 |.||.x.|| - ||.y.||.| <= ||.x - y.||; definition let X, x, y; func dist(x,y) -> Real equals :: CSSPACE:def 16 ||.x - y.||; end; definition let X, x, y; redefine func dist(x,y); commutativity; end; theorem :: CSSPACE:50 dist(x,x) = 0; theorem :: CSSPACE:51 dist(x,z) <= dist(x,y) + dist(y,z); theorem :: CSSPACE:52 x <> y iff dist(x,y) <> 0; theorem :: CSSPACE:53 dist(x,y) >= 0; theorem :: CSSPACE:54 x <> y iff dist(x,y) > 0; theorem :: CSSPACE:55 dist(x,y) = sqrt |.((x-y) .|. (x-y)).|; theorem :: CSSPACE:56 dist(x + y,u + v) <= dist(x,u) + dist(y,v); theorem :: CSSPACE:57 dist(x - y,u - v) <= dist(x,u) + dist(y,v); theorem :: CSSPACE:58 dist(x - z, y - z) = dist(x,y); theorem :: CSSPACE:59 dist(x - z,y - z) <= dist(z,x) + dist(z,y); reserve seq, seq1, seq2, seq3 for sequence of X; reserve n for Nat; definition let X, seq1, seq2; redefine func seq1 + seq2; commutativity; end; theorem :: CSSPACE:60 seq1 + (seq2 + seq3) = (seq1 + seq2) + seq3; theorem :: CSSPACE:61 seq1 is constant & seq2 is constant & seq = seq1 + seq2 implies seq is constant; theorem :: CSSPACE:62 seq1 is constant & seq2 is constant & seq = seq1 - seq2 implies seq is constant; theorem :: CSSPACE:63 seq1 is constant & seq = a * seq1 implies seq is constant; theorem :: CSSPACE:64 seq1 - seq2 = seq1 + -seq2; theorem :: CSSPACE:65 seq = seq + 0.X; theorem :: CSSPACE:66 a * (seq1 + seq2) = a * seq1 + a * seq2; theorem :: CSSPACE:67 (a + b) * seq = a * seq + b * seq; theorem :: CSSPACE:68 (a * b) * seq = a * (b * seq); theorem :: CSSPACE:69 1r * seq = seq; theorem :: CSSPACE:70 (-1r) * seq = - seq; theorem :: CSSPACE:71 seq - x = seq + -x; theorem :: CSSPACE:72 seq1 - seq2 = - (seq2 - seq1); theorem :: CSSPACE:73 seq = seq - 0.X; theorem :: CSSPACE:74 seq = - ( - seq ); theorem :: CSSPACE:75 seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3; theorem :: CSSPACE:76 (seq1 + seq2) - seq3 = seq1 + (seq2 - seq3); theorem :: CSSPACE:77 seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3; theorem :: CSSPACE:78 a * (seq1 - seq2) = a * seq1 - a * seq2; begin :: Complex unitary space of complex sequence definition func cl_scalar -> Function of [:the_set_of_l2ComplexSequences, the_set_of_l2ComplexSequences:], COMPLEX means :: CSSPACE:def 17 for x,y be object st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds it.(x, y) = Sum(seq_id(x)(#)(seq_id(y))*'); end; registration cluster CUNITSTR (# the_set_of_l2ComplexSequences, Zero_( the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences), Add_( the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences), Mult_( the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences), cl_scalar #) -> non empty; end; definition func Complex_l2_Space -> non empty CUNITSTR equals :: CSSPACE:def 18 CUNITSTR (# the_set_of_l2ComplexSequences, Zero_(the_set_of_l2ComplexSequences, Linear_Space_of_ComplexSequences), Add_(the_set_of_l2ComplexSequences, Linear_Space_of_ComplexSequences), Mult_(the_set_of_l2ComplexSequences, Linear_Space_of_ComplexSequences), cl_scalar #); end; theorem :: CSSPACE:79 for l be CLSStruct st the CLSStruct of l is ComplexLinearSpace holds l is ComplexLinearSpace; theorem :: CSSPACE:80 for seq be Complex_Sequence st (for n be Nat holds seq.n=0c ) holds seq is summable & Sum seq = 0c; registration cluster Complex_l2_Space -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital; end; theorem :: CSSPACE:81 |.seq_id(CZeroseq).|(#)|.seq_id(CZeroseq).| is absolutely_summable;