begin
:: deftheorem Def1 defines *' COMPLSP2:def 1 :
for z, b2 being FinSequence of COMPLEX holds
( b2 = z *' iff ( len b2 = len z & ( for i being Nat st 1 <= i & i <= len z holds
b2 . i = (z . i) *' ) ) );
Lm1:
for x being FinSequence of COMPLEX
for c being Element of COMPLEX holds c * x = (multcomplex [;] c,(id COMPLEX )) * x
theorem
theorem
theorem Th3:
theorem
theorem Th5:
Lm4:
for F being complex-valued FinSequence holds F is FinSequence of COMPLEX
theorem Th6:
theorem Th7:
theorem
theorem
theorem
theorem
theorem
theorem Th13:
theorem
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem
theorem
theorem Th24:
theorem Th25:
theorem Th26:
:: deftheorem defines Re COMPLSP2:def 2 :
for z being FinSequence of COMPLEX holds Re z = (1 / 2) * (z + (z *' ));
theorem Th27:
:: deftheorem defines Im COMPLSP2:def 3 :
for z being FinSequence of COMPLEX holds Im z = (- ((1 / 2) * <i> )) * (z - (z *' ));
definition
let x,
y be
FinSequence of
COMPLEX ;
func |(x,y)| -> Element of
COMPLEX equals
((|((Re x),(Re y))| - (<i> * |((Re x),(Im y))|)) + (<i> * |((Im x),(Re y))|)) + |((Im x),(Im y))|;
coherence
((|((Re x),(Re y))| - (<i> * |((Re x),(Im y))|)) + (<i> * |((Im x),(Re y))|)) + |((Im x),(Im y))| is Element of COMPLEX
;
end;
:: deftheorem defines |( COMPLSP2:def 4 :
for x, y being FinSequence of COMPLEX holds |(x,y)| = ((|((Re x),(Re y))| - (<i> * |((Re x),(Im y))|)) + (<i> * |((Im x),(Re y))|)) + |((Im x),(Im y))|;
theorem Th28:
theorem
theorem Th30:
theorem
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem
theorem Th45:
for
C being
Function of
[:COMPLEX ,COMPLEX :],
COMPLEX for
G being
Function of
[:REAL ,REAL :],
REAL for
x1,
y1 being
FinSequence of
COMPLEX for
x2,
y2 being
FinSequence of
REAL st
x1 = x2 &
y1 = y2 &
len x1 = len y2 & ( for
i being
Element of
NAT st
i in dom x1 holds
C . (x1 . i),
(y1 . i) = G . (x2 . i),
(y2 . i) ) holds
C .: x1,
y1 = G .: x2,
y2
theorem
theorem
theorem Th48:
theorem Th49:
theorem
theorem
theorem Th52:
theorem Th53:
Lm2:
for x being FinSequence of COMPLEX holds - (0c (len x)) = 0c (len x)
theorem Th54:
theorem Th55:
theorem
theorem
theorem Th58:
theorem Th59:
theorem Th60:
theorem
theorem
theorem Th63:
theorem Th64:
theorem Th65:
begin
theorem Th66:
theorem Th67:
theorem Th68:
theorem
theorem Th70:
theorem Th71:
theorem Th72:
theorem Th73:
theorem Th74:
theorem Th75:
theorem
theorem
theorem Th78:
theorem Th79:
theorem
theorem