:: CSSPACE semantic presentation
:: 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: :: CSSPACE:1
theorem Th2: :: CSSPACE:2
:: 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:
:: CSSPACE:def 5
for
b1,
b2 being
set st
b1 in COMPLEX &
b2 in the_set_of_ComplexSequences holds
a1 . [b1,b2] = (C_id b1) (#) (seq_id b2);
existence
ex b1 being Function of [:COMPLEX ,the_set_of_ComplexSequences :], the_set_of_ComplexSequences st
for b2, b3 being set st b2 in COMPLEX & b3 in the_set_of_ComplexSequences holds
b1 . [b2,b3] = (C_id b2) (#) (seq_id b3)
by Th2;
uniqueness
for b1, b2 being Function of [:COMPLEX ,the_set_of_ComplexSequences :], the_set_of_ComplexSequences st ( for b3, b4 being set st b3 in COMPLEX & b4 in the_set_of_ComplexSequences holds
b1 . [b3,b4] = (C_id b3) (#) (seq_id b4) ) & ( for b3, b4 being set st b3 in COMPLEX & b4 in the_set_of_ComplexSequences holds
b2 . [b3,b4] = (C_id b3) (#) (seq_id b4) ) holds
b1 = b2
end;
:: deftheorem Def5 defines l_mult CSSPACE:def 5 :
:: deftheorem Def6 defines CZeroseq CSSPACE:def 6 :
theorem Th3: :: CSSPACE:3
theorem Th4: :: CSSPACE:4
theorem Th5: :: CSSPACE:5
Lemma12:
for b1, b2 being VECTOR of CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) holds b1 + b2 = b2 + b1
;
theorem Th6: :: CSSPACE:6
theorem Th7: :: CSSPACE:7
theorem Th8: :: CSSPACE:8
theorem Th9: :: CSSPACE:9
theorem Th10: :: CSSPACE:10
theorem Th11: :: CSSPACE:11
theorem Th12: :: CSSPACE:12
definition
func Linear_Space_of_ComplexSequences -> ComplexLinearSpace equals :: CSSPACE:def 7
CLSStruct(#
the_set_of_ComplexSequences ,
CZeroseq ,
l_add ,
l_mult #);
correctness
coherence
CLSStruct(# the_set_of_ComplexSequences ,CZeroseq ,l_add ,l_mult #) is ComplexLinearSpace;
by Lemma12, Th6, Th7, Th8, Th9, Th10, Th11, Th12, CLVECT_1:1;
end;
:: deftheorem Def7 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: :: CSSPACE:13
:: deftheorem Def11 defines the_set_of_l2ComplexSequences CSSPACE:def 11 :
theorem Th14: :: CSSPACE:14
theorem Th15: :: CSSPACE:15
theorem Th16: :: CSSPACE:16
theorem Th17: :: CSSPACE:17
registration
let c1 be non
empty set ;
let c2 be
Element of
c1;
let c3 be
BinOp of
c1;
let c4 be
Function of
[:COMPLEX ,c1:],
c1;
let c5 be
Function of
[:c1,c1:],
COMPLEX ;
cluster CUNITSTR(#
a1,
a2,
a3,
a4,
a5 #)
-> non
empty ;
coherence
not CUNITSTR(# c1,c2,c3,c4,c5 #) is empty
end;
deffunc H1( CUNITSTR ) -> Element of the carrier of a1 = 0. a1;
:: deftheorem Def12 defines .|. CSSPACE:def 12 :
consider c1 being ComplexLinearSpace;
Lemma27:
the carrier of ((0). c1) = {(0. c1)}
by CLVECT_1:def 5;
reconsider c2 = [:the carrier of ((0). c1),the carrier of ((0). c1):] --> 0c as Function of [:the carrier of ((0). c1),the carrier of ((0). c1):], COMPLEX by FUNCOP_1:57;
Lemma28:
for b1, b2 being VECTOR of ((0). c1) holds c2 . [b1,b2] = 0c
by FUNCOP_1:13;
0. c1 in the carrier of ((0). c1)
by Lemma27, TARSKI:def 1;
then Lemma29:
c2 . [(0. c1),(0. c1)] = 0c
by Lemma28;
Lemma30:
for b1 being VECTOR of ((0). c1) holds
( 0 <= Re (c2 . [b1,b1]) & Im (c2 . [b1,b1]) = 0 )
Lemma31:
for b1, b2 being VECTOR of ((0). c1) holds c2 . [b1,b2] = (c2 . [b2,b1]) *'
Lemma32:
for b1, b2, b3 being VECTOR of ((0). c1) holds c2 . [(b1 + b2),b3] = (c2 . [b1,b3]) + (c2 . [b2,b3])
Lemma33:
for b1, b2 being VECTOR of ((0). c1)
for b3 being Complex holds c2 . [(b3 * b1),b2] = b3 * (c2 . [b1,b2])
set c3 = CUNITSTR(# the carrier of ((0). c1),the Zero of ((0). c1),the add of ((0). c1),the Mult of ((0). c1),c2 #);
E34:
now
let c4,
c5,
c6 be
Point of
CUNITSTR(# the
carrier of
((0). c1),the
Zero of
((0). c1),the
add of
((0). c1),the
Mult of
((0). c1),
c2 #);
let c7 be
Complex;
thus
(
c4 .|. c4 = 0c iff
c4 = H1(
CUNITSTR(# the
carrier of
((0). c1),the
Zero of
((0). c1),the
add of
((0). c1),the
Mult of
((0). c1),
c2 #)) )
proof
H1(
CUNITSTR(# the
carrier of
((0). c1),the
Zero of
((0). c1),the
add of
((0). c1),the
Mult of
((0). c1),
c2 #)) =
the
Zero of
CUNITSTR(# the
carrier of
((0). c1),the
Zero of
((0). c1),the
add of
((0). c1),the
Mult of
((0). c1),
c2 #)
.=
0. ((0). c1)
.=
0. c1
by CLVECT_1:31
;
hence
(
c4 .|. c4 = 0c iff
c4 = H1(
CUNITSTR(# the
carrier of
((0). c1),the
Zero of
((0). c1),the
add of
((0). c1),the
Mult of
((0). c1),
c2 #)) )
by Lemma27, Lemma29, TARSKI:def 1;
end;
thus
( 0
<= Re (c4 .|. c4) & 0
= Im (c4 .|. c4) )
by Lemma30;
thus
c4 .|. c5 = (c5 .|. c4) *'
by Lemma31;
thus
(c4 + c5) .|. c6 = (c4 .|. c6) + (c5 .|. c6)
thus
(c7 * c4) .|. c5 = c7 * (c4 .|. c5)
end;
:: deftheorem Def13 defines ComplexUnitarySpace-like CSSPACE:def 13 :
theorem Th18: :: CSSPACE:18
theorem Th19: :: CSSPACE:19
theorem Th20: :: CSSPACE:20
theorem Th21: :: CSSPACE:21
theorem Th22: :: CSSPACE:22
theorem Th23: :: CSSPACE:23
theorem Th24: :: CSSPACE:24
theorem Th25: :: CSSPACE:25
theorem Th26: :: CSSPACE:26
theorem Th27: :: CSSPACE:27
theorem Th28: :: CSSPACE:28
theorem Th29: :: CSSPACE:29
theorem Th30: :: CSSPACE:30
theorem Th31: :: CSSPACE:31
theorem Th32: :: CSSPACE:32
theorem Th33: :: CSSPACE:33
theorem Th34: :: CSSPACE:34
theorem Th35: :: CSSPACE:35
Lemma51:
for b1 being ComplexUnitarySpace
for b2, b3 being Complex
for b4, b5 being Point of b1 holds ((b2 * b4) + (b3 * b5)) .|. ((b2 * b4) + (b3 * b5)) = ((((b2 * (b2 *' )) * (b4 .|. b4)) + ((b2 * (b3 *' )) * (b4 .|. b5))) + (((b2 *' ) * b3) * (b5 .|. b4))) + ((b3 * (b3 *' )) * (b5 .|. b5))
theorem Th36: :: CSSPACE:36
theorem Th37: :: CSSPACE:37
:: deftheorem Def14 defines are_orthogonal CSSPACE:def 14 :
theorem Th38: :: CSSPACE:38
theorem Th39: :: CSSPACE:39
theorem Th40: :: CSSPACE:40
theorem Th41: :: CSSPACE:41
theorem Th42: :: CSSPACE:42
theorem Th43: :: CSSPACE:43
:: deftheorem Def15 defines ||. CSSPACE:def 15 :
theorem Th44: :: CSSPACE:44
theorem Th45: :: CSSPACE:45
theorem Th46: :: CSSPACE:46
theorem Th47: :: CSSPACE:47
theorem Th48: :: CSSPACE:48
theorem Th49: :: CSSPACE:49
theorem Th50: :: CSSPACE:50
theorem Th51: :: CSSPACE:51
:: deftheorem Def16 defines dist CSSPACE:def 16 :
theorem Th52: :: CSSPACE:52
theorem Th53: :: CSSPACE:53
theorem Th54: :: CSSPACE:54
theorem Th55: :: CSSPACE:55
theorem Th56: :: CSSPACE:56
theorem Th57: :: CSSPACE:57
theorem Th58: :: CSSPACE:58
theorem Th59: :: CSSPACE:59
theorem Th60: :: CSSPACE:60
theorem Th61: :: CSSPACE:61
theorem Th62: :: CSSPACE:62
:: deftheorem Def17 defines - CSSPACE:def 17 :
:: deftheorem Def18 defines + CSSPACE:def 18 :
theorem Th63: :: CSSPACE:63
theorem Th64: :: CSSPACE:64
theorem Th65: :: CSSPACE:65
theorem Th66: :: CSSPACE:66
theorem Th67: :: CSSPACE:67
theorem Th68: :: CSSPACE:68
theorem Th69: :: CSSPACE:69
theorem Th70: :: CSSPACE:70
theorem Th71: :: CSSPACE:71
theorem Th72: :: CSSPACE:72
theorem Th73: :: CSSPACE:73
theorem Th74: :: CSSPACE:74
theorem Th75: :: CSSPACE:75
theorem Th76: :: CSSPACE:76
theorem Th77: :: CSSPACE:77
theorem Th78: :: CSSPACE:78
theorem Th79: :: CSSPACE:79
theorem Th80: :: CSSPACE:80
theorem Th81: :: CSSPACE:81
theorem Th82: :: CSSPACE:82
theorem Th83: :: CSSPACE:83
theorem Th84: :: CSSPACE:84
theorem Th85: :: CSSPACE:85
theorem Th86: :: CSSPACE:86
definition
func cl_scalar -> Function of
[:the_set_of_l2ComplexSequences ,the_set_of_l2ComplexSequences :],
COMPLEX means :: CSSPACE:def 19
for
b1,
b2 being
set st
b1 in the_set_of_l2ComplexSequences &
b2 in the_set_of_l2ComplexSequences holds
a1 . [b1,b2] = Sum ((seq_id b1) (#) ((seq_id b2) *' ));
existence
ex b1 being Function of [:the_set_of_l2ComplexSequences ,the_set_of_l2ComplexSequences :], COMPLEX st
for b2, b3 being set st b2 in the_set_of_l2ComplexSequences & b3 in the_set_of_l2ComplexSequences holds
b1 . [b2,b3] = Sum ((seq_id b2) (#) ((seq_id b3) *' ))
by Th86;
uniqueness
for b1, b2 being Function of [:the_set_of_l2ComplexSequences ,the_set_of_l2ComplexSequences :], COMPLEX st ( for b3, b4 being set st b3 in the_set_of_l2ComplexSequences & b4 in the_set_of_l2ComplexSequences holds
b1 . [b3,b4] = Sum ((seq_id b3) (#) ((seq_id b4) *' )) ) & ( for b3, b4 being set st b3 in the_set_of_l2ComplexSequences & b4 in the_set_of_l2ComplexSequences holds
b2 . [b3,b4] = Sum ((seq_id b3) (#) ((seq_id b4) *' )) ) holds
b1 = b2
end;
:: deftheorem Def19 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
end;
definition
func Complex_l2_Space -> non
empty CUNITSTR equals :: CSSPACE:def 20
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 Def20 defines Complex_l2_Space CSSPACE:def 20 :
theorem Th87: :: CSSPACE:87
theorem Th88: :: CSSPACE:88