begin
:: deftheorem Def1 defines the_set_of_ComplexSequences CSSPACE:def 1 :
:: deftheorem Def2 defines seq_id CSSPACE:def 2 :
:: deftheorem Def3 defines C_id CSSPACE:def 3 :
theorem Th1:
theorem Th2:
:: deftheorem Def4 defines l_add CSSPACE:def 4 :
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 :
:: deftheorem Def6 defines CZeroseq CSSPACE:def 6 :
theorem Th3:
theorem
theorem Th5:
theorem Th6:
for
u,
v,
w being
VECTOR of holds
(u + v) + w = u + (v + w)
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
:: deftheorem defines Linear_Space_of_ComplexSequences CSSPACE:def 7 :
:: deftheorem Def8 defines Add_ CSSPACE:def 8 :
:: deftheorem Def9 defines Mult_ CSSPACE:def 9 :
:: deftheorem Def10 defines Zero_ CSSPACE:def 10 :
theorem Th13:
:: deftheorem Def11 defines the_set_of_l2ComplexSequences CSSPACE:def 11 :
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 :
consider V0 being ComplexLinearSpace;
Lm1:
the carrier of ((0). V0) = {(0. V0)}
by CLVECT_1:def 6;
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 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 holds
( 0 <= Re (nilfunc . [u,u]) & Im (nilfunc . [u,u]) = 0 )
by COMPLEX1:12, FUNCOP_1:13;
Lm5:
for u, v being VECTOR of holds nilfunc . [u,v] = (nilfunc . [v,u]) *'
Lm6:
for u, v, w being VECTOR of holds nilfunc . [(u + v),w] = (nilfunc . [u,w]) + (nilfunc . [v,w])
Lm7:
for u, v being VECTOR of
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 ;
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 :
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 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 :
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem defines ||. CSSPACE:def 15 :
theorem Th44:
theorem Th45:
theorem Th46:
theorem
theorem Th48:
theorem Th49:
theorem Th50:
theorem
:: deftheorem defines dist CSSPACE:def 16 :
theorem Th52:
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 Th63:
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 :
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 :
theorem Th87:
theorem