begin
:: deftheorem Def1 defines the_set_of_ComplexSequences CSSPACE:def 1 :
for b1 being non empty set holds
( b1 = the_set_of_ComplexSequences iff for x being set holds
( x in b1 iff x is Complex_Sequence ) );
:: deftheorem Def2 defines seq_id CSSPACE:def 2 :
for z being set st z in the_set_of_ComplexSequences holds
seq_id z = z;
:: deftheorem Def3 defines C_id CSSPACE:def 3 :
for z being set st z in COMPLEX holds
C_id z = z;
theorem Th1:
theorem Th2:
:: deftheorem Def4 defines l_add CSSPACE:def 4 :
for b1 being BinOp of the_set_of_ComplexSequences holds
( b1 = l_add iff for a, b being Element of the_set_of_ComplexSequences holds b1 . a,b = (seq_id a) + (seq_id b) );
definition
func l_mult -> Function of
[:COMPLEX ,the_set_of_ComplexSequences :],
the_set_of_ComplexSequences means :
Def5:
for
z,
x being
set st
z in COMPLEX &
x in the_set_of_ComplexSequences holds
it . z,
x = (C_id z) (#) (seq_id x);
existence
ex b1 being Function of [:COMPLEX ,the_set_of_ComplexSequences :],the_set_of_ComplexSequences st
for z, x being set st z in COMPLEX & x in the_set_of_ComplexSequences holds
b1 . z,x = (C_id z) (#) (seq_id x)
by Th2;
uniqueness
for b1, b2 being Function of [:COMPLEX ,the_set_of_ComplexSequences :],the_set_of_ComplexSequences st ( for z, x being set st z in COMPLEX & x in the_set_of_ComplexSequences holds
b1 . z,x = (C_id z) (#) (seq_id x) ) & ( for z, x being set st z in COMPLEX & x in the_set_of_ComplexSequences holds
b2 . z,x = (C_id z) (#) (seq_id x) ) holds
b1 = b2
end;
:: deftheorem Def5 defines l_mult CSSPACE:def 5 :
for b1 being Function of [:COMPLEX ,the_set_of_ComplexSequences :],the_set_of_ComplexSequences holds
( b1 = l_mult iff for z, x being set st z in COMPLEX & x in the_set_of_ComplexSequences holds
b1 . z,x = (C_id z) (#) (seq_id x) );
:: deftheorem Def6 defines CZeroseq CSSPACE:def 6 :
for b1 being Element of the_set_of_ComplexSequences holds
( b1 = CZeroseq iff for n being Element of NAT holds (seq_id b1) . n = 0c );
theorem Th3:
theorem
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
:: deftheorem defines Linear_Space_of_ComplexSequences CSSPACE:def 7 :
Linear_Space_of_ComplexSequences = CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #);
:: deftheorem Def8 defines Add_ CSSPACE:def 8 :
for X being ComplexLinearSpace
for X1 being Subset of X st X1 is linearly-closed holds
Add_ X1,X = the addF of X || X1;
:: deftheorem Def9 defines Mult_ CSSPACE:def 9 :
for X being ComplexLinearSpace
for X1 being Subset of X st X1 is linearly-closed holds
Mult_ X1,X = the Mult of X | [:COMPLEX ,X1:];
:: deftheorem Def10 defines Zero_ CSSPACE:def 10 :
for X being ComplexLinearSpace
for X1 being Subset of X st X1 is linearly-closed & not X1 is empty holds
Zero_ X1,X = 0. X;
theorem Th13:
:: deftheorem Def11 defines the_set_of_l2ComplexSequences CSSPACE:def 11 :
for b1 being Subset of Linear_Space_of_ComplexSequences holds
( b1 = the_set_of_l2ComplexSequences iff ( not b1 is empty & ( for x being set holds
( x in b1 iff ( x in the_set_of_ComplexSequences & |.(seq_id x).| (#) |.(seq_id x).| is summable ) ) ) ) );
theorem Th14:
theorem
theorem Th16:
theorem
begin
registration
let D be non
empty set ;
let Z be
Element of
D;
let a be
BinOp of
D;
let m be
Function of
[:COMPLEX ,D:],
D;
let s be
Function of
[:D,D:],
COMPLEX ;
cluster CUNITSTR(#
D,
Z,
a,
m,
s #)
-> non
empty ;
coherence
not CUNITSTR(# D,Z,a,m,s #) is empty
;
end;
deffunc H1( CUNITSTR ) -> Element of the carrier of $1 = 0. $1;
:: deftheorem defines .|. CSSPACE:def 12 :
for X being non empty CUNITSTR
for x, y being Point of X holds x .|. y = the scalar of X . x,y;
consider V0 being ComplexLinearSpace;
Lm1:
the carrier of ((0). V0) = {(0. V0)}
by CLVECT_1:def 9;
reconsider nilfunc = [:the carrier of ((0). V0),the carrier of ((0). V0):] --> 0c as Function of [:the carrier of ((0). V0),the carrier of ((0). V0):],COMPLEX ;
Lm2:
for x, y being VECTOR of ((0). V0) holds nilfunc . [x,y] = 0c
by FUNCOP_1:13;
0. V0 in the carrier of ((0). V0)
by Lm1, TARSKI:def 1;
then Lm3:
nilfunc . [(0. V0),(0. V0)] = 0c
by Lm2;
Lm4:
for u being VECTOR of ((0). V0) holds
( 0 <= Re (nilfunc . [u,u]) & Im (nilfunc . [u,u]) = 0 )
by COMPLEX1:12, FUNCOP_1:13;
Lm5:
for u, v being VECTOR of ((0). V0) holds nilfunc . [u,v] = (nilfunc . [v,u]) *'
Lm6:
for u, v, w being VECTOR of ((0). V0) holds nilfunc . [(u + v),w] = (nilfunc . [u,w]) + (nilfunc . [v,w])
Lm7:
for u, v being VECTOR of ((0). V0)
for a being Complex holds nilfunc . [(a * u),v] = a * (nilfunc . [u,v])
set X0 = CUNITSTR(# the carrier of ((0). V0),(0. ((0). V0)),the addF of ((0). V0),the Mult of ((0). V0),nilfunc #);
Lm8:
now
let x,
y,
z be
Point of
CUNITSTR(# the
carrier of
((0). V0),
(0. ((0). V0)),the
addF of
((0). V0),the
Mult of
((0). V0),
nilfunc #);
for a being Complex holds
( ( x .|. x = 0c implies x = H1( CUNITSTR(# the carrier of ((0). V0),(0. ((0). V0)),the addF of ((0). V0),the Mult of ((0). V0),nilfunc #)) ) & ( x = H1( CUNITSTR(# the carrier of ((0). V0),(0. ((0). V0)),the addF of ((0). V0),the Mult of ((0). V0),nilfunc #)) implies x .|. x = 0c ) & 0 <= Re (x .|. x) & 0 = Im (x .|. x) & x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )let a be
Complex;
( ( x .|. x = 0c implies x = H1( CUNITSTR(# the carrier of ((0). V0),(0. ((0). V0)),the addF of ((0). V0),the Mult of ((0). V0),nilfunc #)) ) & ( x = H1( CUNITSTR(# the carrier of ((0). V0),(0. ((0). V0)),the addF of ((0). V0),the Mult of ((0). V0),nilfunc #)) implies x .|. x = 0c ) & 0 <= Re (x .|. x) & 0 = Im (x .|. x) & x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )
H1(
CUNITSTR(# the
carrier of
((0). V0),
(0. ((0). V0)),the
addF of
((0). V0),the
Mult of
((0). V0),
nilfunc #))
= 0. V0
by CLVECT_1:31;
hence
(
x .|. x = 0c iff
x = H1(
CUNITSTR(# the
carrier of
((0). V0),
(0. ((0). V0)),the
addF of
((0). V0),the
Mult of
((0). V0),
nilfunc #)) )
by Lm1, Lm2, TARSKI:def 1;
( 0 <= Re (x .|. x) & 0 = Im (x .|. x) & x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )thus
(
0 <= Re (x .|. x) &
0 = Im (x .|. x) )
by Lm4;
( x .|. y = (y .|. x) *' & (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )thus
x .|. y = (y .|. x) *'
by Lm5;
( (x + y) .|. z = (x .|. z) + (y .|. z) & (a * x) .|. y = a * (x .|. y) )thus
(x + y) .|. z = (x .|. z) + (y .|. z)
(a * x) .|. y = a * (x .|. y)
thus
(a * x) .|. y = a * (x .|. y)
verum
end;
:: deftheorem Def13 defines ComplexUnitarySpace-like CSSPACE:def 13 :
for IT being non empty CUNITSTR holds
( IT is ComplexUnitarySpace-like iff for x, y, w being Point of IT
for a being Complex holds
( ( x .|. x = 0 implies x = 0. IT ) & ( x = 0. IT implies x .|. x = 0 ) & 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) ) );
theorem
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem
theorem Th31:
theorem Th32:
theorem Th33:
theorem
theorem Th35:
Lm9:
for X being ComplexUnitarySpace
for p, q being Complex
for x, y being Point of X holds ((p * x) + (q * y)) .|. ((p * x) + (q * y)) = ((((p * (p *' )) * (x .|. x)) + ((p * (q *' )) * (x .|. y))) + (((p *' ) * q) * (y .|. x))) + ((q * (q *' )) * (y .|. y))
theorem Th36:
theorem Th37:
:: deftheorem Def14 defines are_orthogonal CSSPACE:def 14 :
for X being ComplexUnitarySpace
for x, y being Point of X holds
( x,y are_orthogonal iff x .|. y = 0 );
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem defines ||. CSSPACE:def 15 :
for X being ComplexUnitarySpace
for x being Point of X holds ||.x.|| = sqrt |.(x .|. x).|;
theorem Th44:
theorem Th45:
theorem Th46:
theorem
theorem Th48:
theorem Th49:
theorem Th50:
theorem
:: deftheorem defines dist CSSPACE:def 16 :
for X being ComplexUnitarySpace
for x, y being Point of X holds dist x,y = ||.(x - y).||;
theorem
canceled;
theorem Th53:
theorem
theorem Th55:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
definition
canceled;
canceled;
end;
:: deftheorem CSSPACE:def 17 :
canceled;
:: deftheorem CSSPACE:def 18 :
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
begin
theorem Th86:
definition
func cl_scalar -> Function of
[:the_set_of_l2ComplexSequences ,the_set_of_l2ComplexSequences :],
COMPLEX means
for
x,
y being
set st
x in the_set_of_l2ComplexSequences &
y in the_set_of_l2ComplexSequences holds
it . x,
y = Sum ((seq_id x) (#) ((seq_id y) *' ));
existence
ex b1 being Function of [:the_set_of_l2ComplexSequences ,the_set_of_l2ComplexSequences :],COMPLEX st
for x, y being set st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds
b1 . x,y = Sum ((seq_id x) (#) ((seq_id y) *' ))
by Th86;
uniqueness
for b1, b2 being Function of [:the_set_of_l2ComplexSequences ,the_set_of_l2ComplexSequences :],COMPLEX st ( for x, y being set st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds
b1 . x,y = Sum ((seq_id x) (#) ((seq_id y) *' )) ) & ( for x, y being set st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds
b2 . x,y = Sum ((seq_id x) (#) ((seq_id y) *' )) ) holds
b1 = b2
end;
:: deftheorem defines cl_scalar CSSPACE:def 19 :
for b1 being Function of [:the_set_of_l2ComplexSequences ,the_set_of_l2ComplexSequences :],COMPLEX holds
( b1 = cl_scalar iff for x, y being set st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds
b1 . x,y = Sum ((seq_id x) (#) ((seq_id y) *' )) );
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 ;
coherence
not 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 #) is empty
by Def11;
end;
definition
func Complex_l2_Space -> non
empty CUNITSTR equals
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 #);
correctness
coherence
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 #) is non empty CUNITSTR ;
;
end;
:: deftheorem defines Complex_l2_Space CSSPACE:def 20 :
Complex_l2_Space = 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 #);
theorem Th87:
theorem