:: Basic Properties of Circulant Matrices and Anti-circular Matrices
:: by Xiaopeng Yue and Xiquan Liang
::
:: Received August 26, 2008
:: Copyright (c) 2008-2019 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, SUBSET_1, VECTSP_1, FINSEQ_1, MATRIX_1, NAT_1, XXREAL_0,
ARYTM_1, INT_1, ARYTM_3, CARD_1, ZFMISC_1, GROUP_1, RELAT_1, FUNCT_1,
TARSKI, STRUCT_0, ALGSTR_0, FUNCOP_1, FVSUM_1, SUPINF_2, FINSEQ_2,
TREES_1, XBOOLE_0, QC_LANG1, INCSP_1, PARTFUN1, MESFUNC1, MATRIX16;
notations MATRIX_0, VECTSP_1, GROUP_1, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1,
TARSKI, FINSEQ_1, FINSEQ_2, FVSUM_1, FUNCT_1, STRUCT_0, BINOP_1,
XXREAL_0, MATRIX_1, FUNCOP_1, INT_1, NUMBERS, XCMPLX_0, MATRIX_3,
MATRIX_4, MATRIX_6, RELAT_1, ALGSTR_0, PARTFUN1, MATRIX13;
constructors REAL_1, MATRIX_6, MATRIX13, POLYNOM1, FVSUM_1, MATRIX_0,
MATRIX_1, MATRIX_4;
registrations STRUCT_0, INT_1, RELSET_1, VECTSP_1, FINSEQ_2, XXREAL_0,
FUNCOP_1, XREAL_0, XBOOLE_0, FUNCT_1, ORDINAL1, MATRIX_0, MATRIX_6;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: Basic Properties of Circulant Matrices
reserve i,j,k,n,l for Element of NAT,
K for Field,
a,b,c for Element of K,
p ,q for FinSequence of K,
M1,M2,M3 for Matrix of n,K;
theorem :: MATRIX16:1
(1_K)*p=p;
theorem :: MATRIX16:2
(-1_K)*p=-p;
definition
let K be set;
let M be Matrix of K;
let p be FinSequence;
pred M is_line_circulant_about p means
:: MATRIX16:def 1
len p = width M & for i,j be
Nat st [i,j] in Indices M holds M*(i,j) = p.((j-i mod len p)+1);
end;
definition
let K be set;
let M be Matrix of K;
attr M is line_circulant means
:: MATRIX16:def 2
ex p being FinSequence of K st len p= width M & M is_line_circulant_about p;
end;
definition
let K be non empty set;
let p be FinSequence of K;
attr p is first-line-of-circulant means
:: MATRIX16:def 3
ex M being Matrix of len p,K st M is_line_circulant_about p;
end;
definition
let K be set;
let M be Matrix of K;
let p be FinSequence;
pred M is_col_circulant_about p means
:: MATRIX16:def 4
len p = len M & for i,j be Nat
st [i,j] in Indices M holds M*(i,j)=p.((i-j mod len p)+1);
end;
definition
let K be set;
let M be Matrix of K;
attr M is col_circulant means
:: MATRIX16:def 5
ex p being FinSequence of K st len p = len M & M is_col_circulant_about p;
end;
definition
let K be non empty set;
let p be FinSequence of K;
attr p is first-col-of-circulant means
:: MATRIX16:def 6
ex M being Matrix of len p,K st M is_col_circulant_about p;
end;
definition
let K be non empty set, p be FinSequence of K;
assume
p is first-line-of-circulant;
func LCirc(p) -> Matrix of len p,K means
:: MATRIX16:def 7
it is_line_circulant_about p;
end;
definition
let K be non empty set, p be FinSequence of K;
assume
p is first-col-of-circulant;
func CCirc(p) -> Matrix of len p,K means
:: MATRIX16:def 8
it is_col_circulant_about p;
end;
registration
let K be Field;
cluster first-line-of-circulant first-col-of-circulant for FinSequence of K;
end;
registration
let K,n;
cluster 0.(K,n) -> line_circulant col_circulant;
end;
registration
let K;
let n;
let a be Element of K;
cluster (n,n)-->a -> line_circulant for Matrix of n,K;
cluster (n,n)-->a -> col_circulant for Matrix of n,K;
end;
registration
let K;
cluster line_circulant col_circulant for Matrix of K;
end;
reserve D for non empty set,
t for FinSequence of D,
A for Matrix of n,D;
theorem :: MATRIX16:3
A is line_circulant & n>0 implies A@ is col_circulant;
theorem :: MATRIX16:4
A is_line_circulant_about t & n>0 implies t = Line(A,1);
theorem :: MATRIX16:5
A is line_circulant & [i,j] in [:Seg n, Seg n:] & k=i+1 & l=j+1 & i0 implies A@ is line_circulant;
theorem :: MATRIX16:18
A is_col_circulant_about t & n>0 implies t = Col(A,1);
theorem :: MATRIX16:19
A is col_circulant & [i,j] in [:Seg n, Seg n:] & k=i+1 & l=j+1 & i0 implies 1.(K,n) is col_circulant;
theorem :: MATRIX16:40
n>0 implies 1.(K,n) is line_circulant;
theorem :: MATRIX16:41
p is first-line-of-circulant implies a*p is first-line-of-circulant;
theorem :: MATRIX16:42
p is first-line-of-circulant implies LCirc(a*p) =a*(LCirc p);
theorem :: MATRIX16:43
p is first-line-of-circulant implies a*(LCirc p)+b*(LCirc p)=LCirc((a+ b)*p);
theorem :: MATRIX16:44
p is first-line-of-circulant & q is first-line-of-circulant & len p =
len q implies a*(LCirc p)+a*(LCirc q)=LCirc(a*(p+q));
theorem :: MATRIX16:45
p is first-line-of-circulant & q is first-line-of-circulant & len p =
len q implies a*(LCirc p)+b*(LCirc q)=LCirc(a*p+b*q);
theorem :: MATRIX16:46
p is first-col-of-circulant implies a*p is first-col-of-circulant;
theorem :: MATRIX16:47
p is first-col-of-circulant implies CCirc(a*p)=a*(CCirc p);
theorem :: MATRIX16:48
p is first-col-of-circulant implies a*(CCirc p)+b*(CCirc p)=CCirc((a+b )*p);
theorem :: MATRIX16:49
p is first-col-of-circulant & q is first-col-of-circulant & len p =
len q & len p > 0 implies a*(CCirc p)+a*(CCirc q)=CCirc(a*(p+q));
theorem :: MATRIX16:50
p is first-col-of-circulant & q is first-col-of-circulant & len p =
len q implies a*(CCirc p)+b*(CCirc q)=CCirc(a*p+b*q);
notation
let K be set;
let M be Matrix of K;
synonym M is circulant for M is line_circulant;
end;
begin :: Basic Properties of Anti-circular Matrices
definition
let K be Field;
let M1 be Matrix of K;
let p be FinSequence of K;
pred M1 is_anti-circular_about p means
:: MATRIX16:def 9
len p=width M1 & (for i,j be
Nat st [i,j] in Indices M1 & i<=j holds M1*(i,j)=p.((j-i mod len p)+1)) & for i
,j be Nat st [i,j] in Indices M1 & i>=j holds M1*(i,j)=(-p).((j-i mod len p)+1)
;
end;
definition
let K be Field;
let M be Matrix of K;
attr M is anti-circular means
:: MATRIX16:def 10
ex p being FinSequence of K st len p= width M & M is_anti-circular_about p;
end;
definition
let K be Field;
let p be FinSequence of K;
attr p is first-line-of-anti-circular means
:: MATRIX16:def 11
ex M being Matrix of len p,K st M is_anti-circular_about p;
end;
definition
let K be Field, p be FinSequence of K;
assume
p is first-line-of-anti-circular;
func ACirc(p) -> Matrix of len p,K means
:: MATRIX16:def 12
it is_anti-circular_about p;
end;
theorem :: MATRIX16:51
M1 is anti-circular implies a*M1 is anti-circular;
theorem :: MATRIX16:52
M1 is anti-circular & M2 is anti-circular implies M1+M2 is anti-circular;
theorem :: MATRIX16:53
for K being Fanoian Field, n,i,j being Nat, M1 being Matrix of n,K st
[i,j] in Indices M1 & i=j & M1 is anti-circular holds M1*(i,j)=0.K;
theorem :: MATRIX16:54
M1 is anti-circular & [i,j] in [:Seg n, Seg n:] & k=i+1 & l=j+1 & i0 implies p = Line(M1,1);
theorem :: MATRIX16:58
p is first-line-of-anti-circular implies -p is first-line-of-anti-circular;
theorem :: MATRIX16:59
p is first-line-of-anti-circular implies ACirc(-p) =-(ACirc(p));
theorem :: MATRIX16:60
p is first-line-of-anti-circular & q is
first-line-of-anti-circular & len p = len q implies p+q is
first-line-of-anti-circular;
theorem :: MATRIX16:61
p is first-line-of-anti-circular & q is
first-line-of-anti-circular & len p = len q implies ACirc(p+q) = ACirc(p)+ACirc
(q);
theorem :: MATRIX16:62
p is first-line-of-anti-circular implies a*p is first-line-of-anti-circular;
theorem :: MATRIX16:63
p is first-line-of-anti-circular implies ACirc(a*p) =a*(ACirc p);
theorem :: MATRIX16:64
p is first-line-of-anti-circular implies a*(ACirc p)+b*(ACirc p)=ACirc
((a+b)*p);
theorem :: MATRIX16:65
p is first-line-of-anti-circular & q is first-line-of-anti-circular &
len p = len q implies a*(ACirc p)+a*(ACirc q)=ACirc(a*(p+q));
theorem :: MATRIX16:66
p is first-line-of-anti-circular & q is first-line-of-anti-circular &
len p = len q implies a*(ACirc p)+b*(ACirc q)=ACirc(a*p+b*q);
registration
let K,n;
cluster 0.(K,n) -> anti-circular;
end;