:: The Inner Product and Conjugate of Matrix of Complex Numbers
:: by Wenpai Chang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received October 10, 2005
:: Copyright (c) 2005-2021 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 NUMBERS, NAT_1, SUBSET_1, FINSEQ_2, MATRIX_1, ARYTM_3, FINSEQ_1,
TREES_1, RELAT_1, CARD_1, XXREAL_0, ZFMISC_1, XCMPLX_0, COMPLFLD,
MATRIX_5, ARYTM_1, COMPLEX1, QC_LANG1, FUNCT_1, RVSUM_1, BINOP_2, TARSKI,
XBOOLE_0, CARD_3, INCSP_1, FUNCOP_1, SETWISEO, ORDINAL4, PARTFUN1,
MATRIXC1, FUNCT_7;
notations TARSKI, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, FUNCT_1,
RELSET_1, FUNCT_2, ZFMISC_1, NAT_D, PARTFUN1, BINOP_1, FUNCOP_1, NAT_1,
FINSEQ_1, FINSEQOP, SEQ_4, COMPLEX1, RVSUM_1, FINSEQ_2, BINOP_2,
MATRIX_5, MATRIX_0, MATRIX_3, MATRIX_4, RLVECT_1, COMPLSP2, SETWOP_2,
COMPLFLD, STRUCT_0, GROUP_1;
constructors SETWISEO, FINSOP_1, MATRIX_3, MATRIX_4, MATRIX_5, SEQ_4, BINOP_2,
BINOP_1, RVSUM_1, NAT_D, RELSET_1, COMPLSP2, PRE_POLY, REAL_1;
registrations XBOOLE_0, FUNCT_1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1,
BINOP_2, FINSEQ_2, COMPLFLD, MATRIX_0, VALUED_0, RELSET_1, XREAL_0,
ORDINAL1, MEMBERED;
requirements NUMERALS, SUBSET, REAL, ARITHM;
begin
reserve i,j,n,k for Nat,
a for Element of COMPLEX,
R1,R2 for Element of i-tuples_on COMPLEX;
definition
let M be Matrix of COMPLEX;
func M*' -> Matrix of COMPLEX means
:: MATRIXC1:def 1
len it=len M & width it=width M &
for i,j being Nat st [i,j] in Indices M holds it*(i,j) = (M*(i,j))*';
involutiveness;
end;
theorem :: MATRIXC1:1
for M be tabular FinSequence holds [i,j] in Indices M iff 1<= i &
i<=len M & 1<=j & j<=width M;
::$CT
theorem :: MATRIXC1:3
for a being Complex,M being Matrix of COMPLEX holds len (a
*M)=len M & width (a*M)=width M;
theorem :: MATRIXC1:4
for i,j being Nat,a being Complex,M being Matrix of
COMPLEX st [i,j] in Indices M holds (a*M)*(i,j) = a*(M*(i,j));
theorem :: MATRIXC1:5
for a being Complex,M being Matrix of COMPLEX holds (a*M)
*' = a*'*(M*');
theorem :: MATRIXC1:6
for M1,M2 being Matrix of COMPLEX holds len (M1+M2)=len M1 &
width (M1+M2)=width M1;
theorem :: MATRIXC1:7
for i,j being Nat,M1,M2 being Matrix of COMPLEX st [i,j] in
Indices M1 holds (M1+M2)*(i,j) = M1*(i,j) + M2*(i,j);
theorem :: MATRIXC1:8
for M1,M2 being Matrix of COMPLEX st len M1=len M2 & width M1=width M2
holds (M1 + M2)*' = M1*' + M2*';
theorem :: MATRIXC1:9
for M being Matrix of COMPLEX holds len (-M)=len M & width (-M)= width M;
theorem :: MATRIXC1:10
for i,j being Nat,M being Matrix of COMPLEX st [i,j] in Indices
M holds (-M)*(i,j)= -(M*(i,j));
theorem :: MATRIXC1:11
for M being Matrix of COMPLEX holds (-1)*M = -M;
theorem :: MATRIXC1:12
for M being Matrix of COMPLEX holds (-M)*' = -(M*');
theorem :: MATRIXC1:13
for M1,M2 being Matrix of COMPLEX holds len (M1-M2)=len M1 &
width (M1-M2)=width M1;
theorem :: MATRIXC1:14
for i,j being Nat,M1,M2 be Matrix of COMPLEX st len M1=len M2 &
width M1=width M2 & [i,j] in Indices M1 holds (M1-M2)*(i,j)=(M1*(i,j)) - (M2*(i
,j));
theorem :: MATRIXC1:15
for M1,M2 being Matrix of COMPLEX st len M1=len M2 & width M1=width M2
holds (M1 - M2)*' = M1*' - M2*';
definition
let M be Matrix of COMPLEX;
func M@" -> Matrix of COMPLEX equals
:: MATRIXC1:def 2
(M@)*';
end;
definition
let x be FinSequence of COMPLEX;
assume
len x > 0;
func FinSeq2Matrix x -> Matrix of COMPLEX means
:: MATRIXC1:def 3
len it = len x & width it = 1 & for j st j in Seg len x holds it.j =<*x.j*>;
end;
definition
let M be Matrix of COMPLEX;
func Matrix2FinSeq M -> FinSequence of COMPLEX equals
:: MATRIXC1:def 4
Col(M,1);
end;
definition
let F1,F2 be FinSequence of COMPLEX;
func mlt(F1,F2) -> FinSequence of COMPLEX equals
:: MATRIXC1:def 5
multcomplex.:(F1,F2);
commutativity;
end;
definition
let M be Matrix of COMPLEX;
let F be FinSequence of COMPLEX;
func M*F -> FinSequence of COMPLEX means
:: MATRIXC1:def 6
len it = len M & for i st i in Seg len M holds it.i=Sum mlt(Line(M,i),F);
end;
theorem :: MATRIXC1:16
a*mlt(R1,R2) = mlt(a*R1,R2);
definition
let M be Matrix of COMPLEX;
let a be Complex;
func M*a -> Matrix of COMPLEX equals
:: MATRIXC1:def 7
a*M;
end;
theorem :: MATRIXC1:17
for a being Element of COMPLEX,M being Matrix of COMPLEX holds (M*a)*'
= a*'*(M*');
theorem :: MATRIXC1:18
for F1,F2 being FinSequence of COMPLEX,i being Nat holds i in
dom mlt(F1,F2) implies mlt(F1,F2).i = F1.i * F2.i;
definition
let i be Element of NAT, R1,R2 be Element of i-tuples_on COMPLEX;
redefine func mlt(R1,R2) -> Element of i-tuples_on COMPLEX;
end;
theorem :: MATRIXC1:19
mlt(R1,R2).j = R1.j * R2.j;
::$CT
theorem :: MATRIXC1:21
for F being FinSequence of COMPLEX ex G being sequence of
COMPLEX st for n being Nat st 1<= n & n<=len F holds G.n=F.n;
theorem :: MATRIXC1:22
for F being FinSequence of COMPLEX st len (F*') >= 1 holds
addcomplex $$ (F*') = (addcomplex $$ F)*';
theorem :: MATRIXC1:23
for F being FinSequence of COMPLEX st len F >= 1 holds Sum(F*') = (Sum F)*';
theorem :: MATRIXC1:24
for x,y being FinSequence of COMPLEX st len x=len y holds (mlt(x
,(y*')))*' = mlt(y,(x*'));
theorem :: MATRIXC1:25
for x,y being FinSequence of COMPLEX,a being Element of COMPLEX
st len x=len y holds (mlt(x,a*y)) = a*mlt(x,y);
theorem :: MATRIXC1:26
for x,y being FinSequence of COMPLEX,a being Element of COMPLEX
st len x=len y holds mlt(a*x,y) = a*mlt(x,y);
theorem :: MATRIXC1:27
for x,y being FinSequence of COMPLEX st len x=len y holds (mlt(x
,y))*' = mlt(x*',y*');
theorem :: MATRIXC1:28
for F being FinSequence of COMPLEX,a being Element of COMPLEX
holds Sum(a*F) = a*(Sum F);
definition
let x be FinSequence of REAL;
func FR2FC(x) -> FinSequence of COMPLEX equals
:: MATRIXC1:def 8
x;
end;
theorem :: MATRIXC1:29
for R being FinSequence of REAL, F being FinSequence of COMPLEX st R =
F & len R >= 1 holds addreal $$ R = addcomplex $$ F;
theorem :: MATRIXC1:30
for x being FinSequence of REAL, y being FinSequence of COMPLEX st x=y
& len x >=1 holds Sum x = Sum y;
theorem :: MATRIXC1:31
for F1,F2 being FinSequence of COMPLEX st len F1=len F2 holds
Sum(F1 - F2) = Sum F1 - Sum F2;
theorem :: MATRIXC1:32
for x,y,z being FinSequence of COMPLEX st len x=len y & len y=len z
holds mlt((x-y),z) = mlt(x,z)-mlt(y,z);
theorem :: MATRIXC1:33
for x,y,z being FinSequence of COMPLEX st len x=len y & len y=
len z holds mlt(x,y-z) = mlt(x,y)-mlt(x,z);
theorem :: MATRIXC1:34
for x,y,z being FinSequence of COMPLEX st len x=len y & len y=len z
holds mlt(x,y+z) = mlt(x,y)+mlt(x,z);
theorem :: MATRIXC1:35
for x,y,z being FinSequence of COMPLEX st len x=len y & len y=
len z holds mlt((x+y),z) = mlt(x,z)+mlt(y,z);
theorem :: MATRIXC1:36
for F1,F2 being FinSequence of COMPLEX st len F1=len F2 holds
Sum(F1 + F2) = Sum F1 + Sum F2;
theorem :: MATRIXC1:37
for x1,y1 being FinSequence of COMPLEX for x2,y2 being
FinSequence of REAL st x1 = x2 & y1 = y2 & len x1=len y2 holds multcomplex.:(x1
,y1) = multreal.:(x2,y2);
theorem :: MATRIXC1:38
for x,y being FinSequence of REAL st len x=len y holds FR2FC mlt(x,y)=
mlt(FR2FC x,FR2FC y);
theorem :: MATRIXC1:39
for x,y being FinSequence of COMPLEX st len x=len y holds |( x,y
)| = Sum mlt(x,(y*'));
theorem :: MATRIXC1:40
for i,j being Nat,M1,M2 being Matrix of COMPLEX st width M1=width M2 &
j in Seg len M1 holds Line(M1+M2,j)=Line(M1,j)+Line(M2,j);
theorem :: MATRIXC1:41
for M being Matrix of COMPLEX st i in Seg len M holds Line(M,i)=
(Line(M*',i))*';
theorem :: MATRIXC1:42
for F being FinSequence of COMPLEX,M being Matrix of COMPLEX st
len F=width M holds mlt(F,(Line((M*'),i))*') = mlt(Line((M*'),i),(F*'))*';
theorem :: MATRIXC1:43
for F being FinSequence of COMPLEX,M being Matrix of COMPLEX st
len F = width M & len F >= 1 holds (M*F)*'=(M*')*(F*');
theorem :: MATRIXC1:44
for F1,F2,F3 being FinSequence of COMPLEX st len F1 = len F2 & len F2
= len F3 holds mlt(F1,mlt(F2,F3)) = mlt(mlt(F1,F2),F3);
theorem :: MATRIXC1:45
for F being FinSequence of COMPLEX holds Sum -F = -(Sum F);
theorem :: MATRIXC1:46
for F1,F2 being FinSequence of COMPLEX holds Sum(F1^F2) = Sum F1 + Sum F2;
definition
let M be Matrix of COMPLEX;
func LineSum M -> FinSequence of COMPLEX means
:: MATRIXC1:def 9
len it=len M & for i being Nat st i in Seg len M holds it.i=Sum Line(M,i);
end;
definition
let M be Matrix of COMPLEX;
func ColSum M -> FinSequence of COMPLEX means
:: MATRIXC1:def 10
len it=width M & for j
being Nat st j in Seg width M holds it.j=Sum (Col(M,j));
end;
theorem :: MATRIXC1:47
for F being FinSequence of COMPLEX holds len F = 1 implies Sum F = F.1;
theorem :: MATRIXC1:48
for f,g being FinSequence of COMPLEX,n being Nat st len f = n +
1 & g = f|n holds Sum f = Sum g + f/.(len f);
theorem :: MATRIXC1:49
for M being Matrix of COMPLEX st len M > 0 holds Sum LineSum M = Sum ColSum M
;
definition
let M be Matrix of COMPLEX;
func SumAll M -> Element of COMPLEX equals
:: MATRIXC1:def 11
Sum LineSum M;
end;
theorem :: MATRIXC1:50
for M being Matrix of COMPLEX holds ColSum M = LineSum(M@);
theorem :: MATRIXC1:51
for M being Matrix of COMPLEX st len M > 0 holds SumAll M = SumAll (M@);
definition
let x,y be FinSequence of COMPLEX,M be Matrix of COMPLEX;
assume that
len x=len M and
len y=width M;
func QuadraticForm(x,M,y) -> Matrix of COMPLEX means
:: MATRIXC1:def 12
len it = len x & width it=len y &
for i,j being Nat st [i,j] in Indices M holds it*(i,j)=(x.i)
*(M*(i,j))*((y.j)*');
end;
theorem :: MATRIXC1:52
for x,y being FinSequence of COMPLEX,M being Matrix of COMPLEX
st len x = len M & len y = width M & len y > 0 holds (QuadraticForm(x,M,y))@ =
(QuadraticForm(y,M@",x))*';
theorem :: MATRIXC1:53
for x,y being FinSequence of COMPLEX,M being Matrix of COMPLEX
st len x=len M & len y =width M holds (QuadraticForm(x,M,y))*'=QuadraticForm(x
*',M*',y*');
theorem :: MATRIXC1:54
for x,y being FinSequence of COMPLEX st len x=len y & 0 < len y
holds |(x,y)|=(|(y,x)|)*';
theorem :: MATRIXC1:55
for x,y being FinSequence of COMPLEX st len x=len y & 0 < len y
holds (|(x,y)|)*'=|(x*',y*')|;
theorem :: MATRIXC1:56
for M being Matrix of COMPLEX st width M > 0 holds (M@)*' =(M*')@;
theorem :: MATRIXC1:57
for x,y being FinSequence of COMPLEX,M being Matrix of COMPLEX
st len x=width M & len y = len M & len x>0 & len y>0 holds |(x,(M@")*y)| =
SumAll QuadraticForm(x,M@,y);
theorem :: MATRIXC1:58
for x,y being FinSequence of COMPLEX,M being Matrix of COMPLEX
st len y=len M & len x =width M & len x>0 & len y>0 holds |(M*x,y)| = SumAll
QuadraticForm(x,M@,y);
theorem :: MATRIXC1:59
for x,y being FinSequence of COMPLEX, M being Matrix of COMPLEX
st len x=width M & len y =len M & width M>0 & len M>0 holds |(M*x,y)| = |(x,(M
@")*y)|;
theorem :: MATRIXC1:60
for x,y being FinSequence of COMPLEX,M being Matrix of COMPLEX st len
x=len M & len y =width M & width M>0 & len M>0 holds |(x,M*y)| = |((M@")*x,y)|;