:: The Inner Product and Conjugate of Finite Sequences of Complex Numbers
:: by Wenpai Chang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received April 25, 2005
:: Copyright (c) 2005-2017 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 SUBSET_1, NUMBERS, FINSEQ_1, FINSEQ_2, ARYTM_3, NAT_1, XXREAL_0,
FUNCT_1, RELAT_1, TARSKI, BINOP_2, FUNCOP_1, ARYTM_1, XCMPLX_0, CARD_1,
COMPLEX1, RVSUM_1, REAL_1, ZFMISC_1, VALUED_0, VALUED_1;
notations TARSKI, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1,
RELAT_1, FUNCT_1, FUNCT_2, ZFMISC_1, PARTFUN1, BINOP_1, FUNCOP_1,
FINSEQ_1, FINSEQOP, VALUED_0, VALUED_1, SEQ_4, COMPLEX1, RVSUM_1,
FINSEQ_2, BINOP_2, MATRIX_5, XXREAL_0, COMSEQ_2;
constructors SETWISEO, REAL_1, BINOP_2, FINSEQOP, SEQ_4, MATRIX_5, BINOP_1,
RVSUM_1, RELSET_1, COMSEQ_2;
registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCT_2, NUMBERS, XCMPLX_0,
BINOP_2, MEMBERED, FINSEQ_2, VALUED_0, VALUED_1, XREAL_0;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: Preliminaries
reserve i,j for Element of NAT,
x,y,z for FinSequence of COMPLEX,
c for Element of COMPLEX,
R,R1,R2 for Element of i-tuples_on COMPLEX;
definition let z be FinSequence of COMPLEX;
redefine func z*' -> FinSequence of COMPLEX means
:: COMPLSP2:def 1
len it = len z & for i being Nat st 1<=i & i<=len z holds it.i = (z.i)*';
end;
theorem :: COMPLSP2:1
i in dom (x+y) implies (x+y).i = x.i + y.i;
theorem :: COMPLSP2:2
i in dom (x-y) implies (x-y).i = x.i - y.i;
definition let i,R1,R2;
redefine func R1 - R2 -> Element of i-tuples_on COMPLEX;
end;
definition let i,R1,R2;
redefine func R1 + R2 -> Element of i-tuples_on COMPLEX;
end;
definition let i, R;
let r be Complex;
redefine func r*R -> Element of i-tuples_on COMPLEX;
end;
theorem :: COMPLSP2:3
for a being Complex, x being complex-valued FinSequence holds
len (a(#)x) = len x;
theorem :: COMPLSP2:4
for x being complex-valued FinSequence holds dom x = dom -x;
theorem :: COMPLSP2:5
for x being complex-valued FinSequence holds len (-x)=len x;
theorem :: COMPLSP2:6
for x1,x2 being complex-valued FinSequence st len x1=len x2 holds
len (x1+x2)=len x1;
theorem :: COMPLSP2:7
for x1,x2 being complex-valued FinSequence st len x1=len x2 holds
len (x1-x2)=len x1;
theorem :: COMPLSP2:8
for f being complex-valued FinSequence holds f is Element of COMPLEX len f;
::$CT 4
theorem :: COMPLSP2:13
for x being FinSequence of COMPLEX holds (-x).i = -x.i;
definition let i,R;
redefine func -R -> Element of i-tuples_on COMPLEX;
end;
theorem :: COMPLSP2:14
c = R.j implies (-R).j = -c;
theorem :: COMPLSP2:15
for a being Complex holds dom(a*x) = dom x;
theorem :: COMPLSP2:16
for i being Nat, a being Complex holds (a*x).i = a*(x.i);
theorem :: COMPLSP2:17
for a being Complex holds (a*x)*' = a*'*(x*');
theorem :: COMPLSP2:18
(R1+R2).j = R1.j + R2.j;
theorem :: COMPLSP2:19
for x1,x2 being FinSequence of COMPLEX st len x1=len x2 holds
(x1 + x2)*' = x1*' + x2*';
theorem :: COMPLSP2:20
(R1-R2).j = R1.j - R2.j;
theorem :: COMPLSP2:21
for x1,x2 being FinSequence of COMPLEX st len x1=len x2 holds
(x1 - x2)*' = x1*' - x2*';
theorem :: COMPLSP2:22
for z being FinSequence of COMPLEX holds (z*')*' = z;
theorem :: COMPLSP2:23
for z being FinSequence of COMPLEX holds (-z)*' = -(z*');
theorem :: COMPLSP2:24
for z being Complex holds z+z*' = 2*(Re z);
theorem :: COMPLSP2:25
for x,y being complex-valued FinSequence st len x=len y holds
(x-y).i = x.i - y.i;
theorem :: COMPLSP2:26
for x,y being complex-valued FinSequence st len x=len y holds
(x+y).i = x.i + y.i;
definition let z be FinSequence of COMPLEX;
func Re z -> FinSequence of REAL equals
:: COMPLSP2:def 2
1/2*(z+z*');
end;
theorem :: COMPLSP2:27
for z being Complex holds z-z*' = 2*(Im z) * *;
definition
let z be FinSequence of COMPLEX;
func Im z -> FinSequence of REAL equals
:: COMPLSP2:def 3
(-1/2***)*(z-z*');
end;
definition
let x,y be FinSequence of COMPLEX;
func |( x,y )| -> Element of COMPLEX equals
:: COMPLSP2:def 4
|(Re x,Re y)| - ***(|(Re x,Im y)|) + ***(|(Im x,Re y)|) + |(Im x,Im y)|;
end;
theorem :: COMPLSP2:28
for x,y,z being complex-valued FinSequence st len x=len y & len y=len z
holds x + (y + z) = x + y + z;
::$CT
theorem :: COMPLSP2:30
for c being Complex, x,y being FinSequence of COMPLEX st
len x=len y holds c*(x+y) = c*x + c*y;
::$CT
theorem :: COMPLSP2:32
for x,y being complex-valued FinSequence st len x=len y & x + y = 0c
(len x) holds x = -y & y = -x;
theorem :: COMPLSP2:33
for x being complex-valued FinSequence holds x + 0c (len x) = x;
theorem :: COMPLSP2:34
for x being complex-valued FinSequence holds x + -x = 0c (len x);
theorem :: COMPLSP2:35
for x,y being complex-valued FinSequence st len x=len y holds
-(x + y) = -x + -y;
theorem :: COMPLSP2:36
for x,y,z being complex-valued FinSequence st len x=len y & len y=len z
holds x - y - z = x - (y + z);
theorem :: COMPLSP2:37
for x,y,z being complex-valued FinSequence st len x=len y & len y=len z
holds x + (y - z) = x + y - z;
::$CT
theorem :: COMPLSP2:39
for x,y being complex-valued FinSequence st len x=len y holds
-(x - y) = -x + y;
theorem :: COMPLSP2:40
for x,y,z being complex-valued FinSequence st
len x=len y & len y=len z holds x - (y - z) = x - y + z;
theorem :: COMPLSP2:41
for c being Complex holds c*(0c (len x)) = 0c (len x);
theorem :: COMPLSP2:42
for c being Complex holds -c*x = c*(-x);
theorem :: COMPLSP2:43
for c being Complex, x,y being FinSequence of COMPLEX st
len x=len y holds c*(x-y) = c*x - c*y;
theorem :: COMPLSP2:44
for x1,y1 being Element of COMPLEX
for x2,y2 being Real st x1 = x2 &
y1 = y2 holds addcomplex.(x1,y1) = addreal.(x2,y2);
reserve C for Function of [:COMPLEX,COMPLEX:],COMPLEX;
reserve G for Function of [:REAL,REAL:],REAL;
theorem :: COMPLSP2:45
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 st i in dom
x1 holds C.(x1.i,y1.i)=G.(x2.i,y2.i)) holds C.:(x1,y1)=G.:(x2,y2);
theorem :: COMPLSP2:46
for x1,y1 being FinSequence of COMPLEX for x2,y2 being FinSequence of
REAL st x1 = x2 & y1 = y2 & len x1=len y2 holds addcomplex.:(x1,y1) = addreal.:
(x2,y2);
::$CT
theorem :: COMPLSP2:48
for x being FinSequence of COMPLEX holds len (Re x)=len x & len (Im x)=len x;
theorem :: COMPLSP2:49
for x,y being FinSequence of COMPLEX st len x=len y holds Re (x+
y) = Re x + Re y & Im(x + y) = Im x + Im y;
theorem :: COMPLSP2:50
for x1,y1 being FinSequence of COMPLEX for x2,y2 being FinSequence of
REAL st x1 = x2 & y1 = y2 & len x1=len y2 holds diffcomplex.:(x1,y1) = diffreal
.:(x2,y2);
::$CT
theorem :: COMPLSP2:52
for x,y being FinSequence of COMPLEX st len x=len y holds
Re(x - y) = Re x - Re y & Im(x - y) = Im x - Im y;
theorem :: COMPLSP2:53
for a, b being Complex holds a*(b*z) = (a*b)*z;
theorem :: COMPLSP2:54
for c being Complex holds (-c)*x = -(c*x);
reserve h for Function of COMPLEX,COMPLEX,
g for Function of REAL,REAL;
theorem :: COMPLSP2:55
for y1 being FinSequence of COMPLEX for y2 being FinSequence of
REAL st len y1=len y2 & (for i st i in dom y1 holds h.(y1.i)=g.(y2.i)) holds h*
y1 = g*y2;
theorem :: COMPLSP2:56
for y1 being FinSequence of COMPLEX for y2 being FinSequence of REAL
st y1 = y2 & len y1=len y2 holds compcomplex*y1 = compreal*y2;
::$CT
theorem :: COMPLSP2:58
for x being FinSequence of COMPLEX holds Re (***x) = -(Im x) &
Im (***x) = Re x;
theorem :: COMPLSP2:59
for x,y being FinSequence of COMPLEX st len x=len y holds
|(***x,y)| = ***(|(x,y)|);
theorem :: COMPLSP2:60
for x,y being FinSequence of COMPLEX st len x=len y holds |(x,
***y)| = -***(|(x,y)|);
theorem :: COMPLSP2:61
for a1 being Element of COMPLEX,y1 being FinSequence of COMPLEX for a2
being Element of REAL,y2 being FinSequence of REAL st a1 = a2 & y1 = y2 & len
y1=len y2 holds (a1 multcomplex)*y1 = (a2 multreal)*y2;
::$CT
theorem :: COMPLSP2:63
for a, b being Complex holds (a+b)*z = a*z + b*z;
theorem :: COMPLSP2:64
for a, b being Complex holds (a-b)*z = a*z - b*z;
theorem :: COMPLSP2:65
for a being Element of COMPLEX,x being FinSequence of COMPLEX
holds Re (a*x) = Re a * Re x - Im a * Im x & Im (a*x) = Im a * Re x + Re a * Im
x;
begin :: The Inner Product and Conjugate of Finite Sequences
theorem :: COMPLSP2:66
for x1,x2,y being FinSequence of COMPLEX st len x1=len x2 & len
x2=len y holds |((x1+x2),y)| = |(x1,y)| + |(x2,y)|;
theorem :: COMPLSP2:67
for x1,x2 being FinSequence of COMPLEX st len x1=len x2 holds
|(-x1, x2)| = -|(x1, x2)|;
theorem :: COMPLSP2:68
for x1,x2 being FinSequence of COMPLEX st len x1=len x2 holds
|(x1, -x2)| = -|(x1, x2)|;
theorem :: COMPLSP2:69
for x1,x2 being FinSequence of COMPLEX st len x1=len x2 holds
|(-x1, -x2)| = |(x1, x2)|;
theorem :: COMPLSP2:70
for x1,x2,x3 being FinSequence of COMPLEX st
len x1=len x2 & len x2=len x3 holds
|(x1-x2, x3)| = |(x1, x3)| - |(x2, x3)|;
theorem :: COMPLSP2:71
for x,y1,y2 being FinSequence of COMPLEX st
len x=len y1 & len y1=len y2 holds |(x, y1+y2)| = |(x, y1)| + |(x, y2)|;
theorem :: COMPLSP2:72
for x,y1,y2 being FinSequence of COMPLEX st len x=len y1 & len y1=len y2
holds |(x, y1-y2)| = |(x, y1)| - |(x, y2)|;
theorem :: COMPLSP2:73
for x1,x2,y1,y2 being FinSequence of COMPLEX st len x1=len x2 &
len x2=len y1 & len y1=len y2 holds
|(x1+x2, y1+y2)| = |(x1, y1)| + |(x1, y2)| + |(x2, y1)| + |(x2, y2)|;
theorem :: COMPLSP2:74
for x1,x2,y1,y2 being FinSequence of COMPLEX st
len x1=len x2 & len x2=len y1 & len y1=len y2 holds
|(x1-x2, y1-y2)| = |(x1, y1)| - |(x1, y2)| - |(x2, y1)| + |(x2, y2)|;
theorem :: COMPLSP2:75
for x,y being FinSequence of COMPLEX holds |(x,y)| = (|(y,x)|)*';
theorem :: COMPLSP2:76
for x,y being FinSequence of COMPLEX st len x=len y holds
|(x+y,x+y)| = |(x,x)| + 2*Re(|(x,y)|) + |(y,y)|;
theorem :: COMPLSP2:77
for x,y being FinSequence of COMPLEX st len x=len y holds
|(x-y, x-y)| = |(x, x)| - 2*Re(|(x, y)|) + |(y, y)|;
theorem :: COMPLSP2:78
for a being Element of COMPLEX, x,y being FinSequence of COMPLEX
st len x=len y holds |(a*x,y)| = a*(|(x,y)|);
theorem :: COMPLSP2:79
for a being Element of COMPLEX, x,y being FinSequence of COMPLEX
st len x=len y holds |(x,a*y)| = (a*')*(|(x,y)|);
theorem :: COMPLSP2:80
for a,b being Element of COMPLEX,x,y,z being FinSequence of COMPLEX st
len x=len y & len y=len z holds |((a*x+b*y), z)| = a*|(x,z)| + b*|(y,z)|;
theorem :: COMPLSP2:81
for a,b being Element of COMPLEX,x,y,z being FinSequence of COMPLEX st
len x=len y & len y=len z holds |(x,a*y+b*z)| = (a*')*|(x,y)| + (b*')*|(x,z)|
;
*