:: Basic Properties of Circulant Matrices and Anti-circular Matrices
:: by Xiaopeng Yue and Xiquan Liang
::
:: Received August 26, 2008
:: Copyright (c) 2008-2011 Association of Mizar Users


begin

Lm1: for n being Element of NAT
for k being Nat st k <= n & k >= 1 holds
(k - 1) mod n = k - 1
proof end;

Lm2: for n, i, j being Nat st i in Seg n & j in Seg n holds
((j - i) mod n) + 1 in Seg n
proof end;

Lm3: for n, i, j being Nat st ( [i,j] in [:(Seg n),(Seg n):] or [j,i] in [:(Seg n),(Seg n):] ) holds
((j - i) mod n) + 1 in Seg n
proof end;

theorem :: MATRIX16:1
for K being Field
for p being FinSequence of K holds (1_ K) * p = p
proof end;

theorem :: MATRIX16:2
for K being Field
for p being FinSequence of K holds (- (1_ K)) * p = - p
proof end;

definition
let K be set ;
let M be Matrix of K;
let p be FinSequence;
pred M is_line_circulant_about p means :Def1: :: MATRIX16:def 1
( len p = width M & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = p . (((j - i) mod (len p)) + 1) ) );
end;

:: deftheorem Def1 defines is_line_circulant_about MATRIX16:def 1 :
for K being set
for M being Matrix of K
for p being FinSequence holds
( M is_line_circulant_about p iff ( len p = width M & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = p . (((j - i) mod (len p)) + 1) ) ) );

definition
let K be set ;
let M be Matrix of K;
attr M is line_circulant means :Def2: :: MATRIX16:def 2
ex p being FinSequence of K st
( len p = width M & M is_line_circulant_about p );
end;

:: deftheorem Def2 defines line_circulant MATRIX16:def 2 :
for K being set
for M being Matrix of K holds
( M is line_circulant iff ex p being FinSequence of K st
( len p = width M & M is_line_circulant_about p ) );

definition
let K be non empty set ;
let p be FinSequence of K;
attr p is first-line-of-circulant means :Def3: :: MATRIX16:def 3
ex M being Matrix of len p,K st M is_line_circulant_about p;
end;

:: deftheorem Def3 defines first-line-of-circulant MATRIX16:def 3 :
for K being non empty set
for p being FinSequence of K holds
( p is first-line-of-circulant iff ex M being Matrix of len p,K st M is_line_circulant_about p );

definition
let K be set ;
let M be Matrix of K;
let p be FinSequence;
pred M is_col_circulant_about p means :Def4: :: MATRIX16:def 4
( len p = len M & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = p . (((i - j) mod (len p)) + 1) ) );
end;

:: deftheorem Def4 defines is_col_circulant_about MATRIX16:def 4 :
for K being set
for M being Matrix of K
for p being FinSequence holds
( M is_col_circulant_about p iff ( len p = len M & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = p . (((i - j) mod (len p)) + 1) ) ) );

definition
let K be set ;
let M be Matrix of K;
attr M is col_circulant means :Def5: :: MATRIX16:def 5
ex p being FinSequence of K st
( len p = len M & M is_col_circulant_about p );
end;

:: deftheorem Def5 defines col_circulant MATRIX16:def 5 :
for K being set
for M being Matrix of K holds
( M is col_circulant iff ex p being FinSequence of K st
( len p = len M & M is_col_circulant_about p ) );

definition
let K be non empty set ;
let p be FinSequence of K;
attr p is first-col-of-circulant means :Def6: :: MATRIX16:def 6
ex M being Matrix of len p,K st M is_col_circulant_about p;
end;

:: deftheorem Def6 defines first-col-of-circulant MATRIX16:def 6 :
for K being non empty set
for p being FinSequence of K holds
( p is first-col-of-circulant iff ex M being Matrix of len p,K st M is_col_circulant_about p );

definition
let K be non empty set ;
let p be FinSequence of K;
assume A1: p is first-line-of-circulant ;
func LCirc p -> Matrix of len p,K means :Def7: :: MATRIX16:def 7
it is_line_circulant_about p;
existence
ex b1 being Matrix of len p,K st b1 is_line_circulant_about p
by A1, Def3;
uniqueness
for b1, b2 being Matrix of len p,K st b1 is_line_circulant_about p & b2 is_line_circulant_about p holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines LCirc MATRIX16:def 7 :
for K being non empty set
for p being FinSequence of K st p is first-line-of-circulant holds
for b3 being Matrix of len p,K holds
( b3 = LCirc p iff b3 is_line_circulant_about p );

definition
let K be non empty set ;
let p be FinSequence of K;
assume A1: p is first-col-of-circulant ;
func CCirc p -> Matrix of len p,K means :Def8: :: MATRIX16:def 8
it is_col_circulant_about p;
existence
ex b1 being Matrix of len p,K st b1 is_col_circulant_about p
by A1, Def6;
uniqueness
for b1, b2 being Matrix of len p,K st b1 is_col_circulant_about p & b2 is_col_circulant_about p holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines CCirc MATRIX16:def 8 :
for K being non empty set
for p being FinSequence of K st p is first-col-of-circulant holds
for b3 being Matrix of len p,K holds
( b3 = CCirc p iff b3 is_col_circulant_about p );

registration
let K be Field;
cluster Relation-like NAT -defined the carrier of K -valued Function-like FinSequence-like first-line-of-circulant first-col-of-circulant FinSequence of the carrier of K;
existence
ex b1 being FinSequence of K st
( b1 is first-line-of-circulant & b1 is first-col-of-circulant )
proof end;
end;

registration
let K be Field;
let n be Element of NAT ;
cluster 0. (K,n) -> line_circulant col_circulant ;
coherence
( 0. (K,n) is line_circulant & 0. (K,n) is col_circulant )
proof end;
end;

registration
let K be Field;
let n be Element of NAT ;
let a be Element of K;
cluster (n,n) --> a -> line_circulant Matrix of n,K;
coherence
for b1 being Matrix of n,K st b1 = (n,n) --> a holds
b1 is line_circulant
proof end;
cluster (n,n) --> a -> col_circulant Matrix of n,K;
coherence
for b1 being Matrix of n,K st b1 = (n,n) --> a holds
b1 is col_circulant
proof end;
end;

registration
let K be Field;
cluster Relation-like NAT -defined the carrier of K * -valued Function-like FinSequence-like Function-yielding tabular line_circulant col_circulant FinSequence of the carrier of K * ;
existence
ex b1 being Matrix of K st
( b1 is line_circulant & b1 is col_circulant )
proof end;
end;

theorem :: MATRIX16:3
for n being Element of NAT
for D being non empty set
for A being Matrix of n,D st A is line_circulant & n > 0 holds
A @ is col_circulant
proof end;

theorem :: MATRIX16:4
for n being Element of NAT
for D being non empty set
for t being FinSequence of D
for A being Matrix of n,D st A is_line_circulant_about t & n > 0 holds
t = Line (A,1)
proof end;

theorem :: MATRIX16:5
for i, j, n, k, l being Element of NAT
for D being non empty set
for A being Matrix of n,D st A is line_circulant & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n holds
A * (i,j) = A * (k,l)
proof end;

theorem Th6: :: MATRIX16:6
for n being Element of NAT
for K being Field
for a being Element of K
for M1 being Matrix of n,K st M1 is line_circulant holds
a * M1 is line_circulant
proof end;

theorem Th7: :: MATRIX16:7
for n being Element of NAT
for K being Field
for M1, M2 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant holds
M1 + M2 is line_circulant
proof end;

theorem Th8: :: MATRIX16:8
for n being Element of NAT
for K being Field
for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds
(M1 + M2) + M3 is line_circulant
proof end;

theorem :: MATRIX16:9
for n being Element of NAT
for K being Field
for a, b being Element of K
for M1, M2 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant holds
(a * M1) + (b * M2) is line_circulant
proof end;

theorem :: MATRIX16:10
for n being Element of NAT
for K being Field
for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds
((a * M1) + (b * M2)) + (c * M3) is line_circulant
proof end;

theorem Th11: :: MATRIX16:11
for n being Element of NAT
for K being Field
for M1 being Matrix of n,K st M1 is line_circulant holds
- M1 is line_circulant
proof end;

theorem :: MATRIX16:12
for n being Element of NAT
for K being Field
for M1, M2 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant holds
M1 - M2 is line_circulant
proof end;

theorem Th13: :: MATRIX16:13
for n being Element of NAT
for K being Field
for a, b being Element of K
for M1, M2 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant holds
(a * M1) - (b * M2) is line_circulant
proof end;

theorem :: MATRIX16:14
for n being Element of NAT
for K being Field
for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds
((a * M1) + (b * M2)) - (c * M3) is line_circulant
proof end;

theorem :: MATRIX16:15
for n being Element of NAT
for K being Field
for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds
((a * M1) - (b * M2)) - (c * M3) is line_circulant
proof end;

theorem :: MATRIX16:16
for n being Element of NAT
for K being Field
for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is line_circulant & M2 is line_circulant & M3 is line_circulant holds
((a * M1) - (b * M2)) + (c * M3) is line_circulant
proof end;

theorem :: MATRIX16:17
for n being Element of NAT
for D being non empty set
for A being Matrix of n,D st A is col_circulant & n > 0 holds
A @ is line_circulant
proof end;

theorem :: MATRIX16:18
for n being Element of NAT
for D being non empty set
for t being FinSequence of D
for A being Matrix of n,D st A is_col_circulant_about t & n > 0 holds
t = Col (A,1)
proof end;

theorem :: MATRIX16:19
for i, j, n, k, l being Element of NAT
for D being non empty set
for A being Matrix of n,D st A is col_circulant & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n holds
A * (i,j) = A * (k,l)
proof end;

theorem Th20: :: MATRIX16:20
for n being Element of NAT
for K being Field
for a being Element of K
for M1 being Matrix of n,K st M1 is col_circulant holds
a * M1 is col_circulant
proof end;

theorem Th21: :: MATRIX16:21
for n being Element of NAT
for K being Field
for M1, M2 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant holds
M1 + M2 is col_circulant
proof end;

theorem Th22: :: MATRIX16:22
for n being Element of NAT
for K being Field
for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds
(M1 + M2) + M3 is col_circulant
proof end;

theorem :: MATRIX16:23
for n being Element of NAT
for K being Field
for a, b being Element of K
for M1, M2 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant holds
(a * M1) + (b * M2) is col_circulant
proof end;

theorem :: MATRIX16:24
for n being Element of NAT
for K being Field
for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds
((a * M1) + (b * M2)) + (c * M3) is col_circulant
proof end;

theorem Th25: :: MATRIX16:25
for n being Element of NAT
for K being Field
for M1 being Matrix of n,K st M1 is col_circulant holds
- M1 is col_circulant
proof end;

theorem :: MATRIX16:26
for n being Element of NAT
for K being Field
for M1, M2 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant holds
M1 - M2 is col_circulant
proof end;

theorem Th27: :: MATRIX16:27
for n being Element of NAT
for K being Field
for a, b being Element of K
for M1, M2 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant holds
(a * M1) - (b * M2) is col_circulant
proof end;

theorem :: MATRIX16:28
for n being Element of NAT
for K being Field
for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds
((a * M1) + (b * M2)) - (c * M3) is col_circulant
proof end;

theorem :: MATRIX16:29
for n being Element of NAT
for K being Field
for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds
((a * M1) - (b * M2)) - (c * M3) is col_circulant
proof end;

theorem :: MATRIX16:30
for n being Element of NAT
for K being Field
for a, b, c being Element of K
for M1, M2, M3 being Matrix of n,K st M1 is col_circulant & M2 is col_circulant & M3 is col_circulant holds
((a * M1) - (b * M2)) + (c * M3) is col_circulant
proof end;

theorem Th31: :: MATRIX16:31
for K being Field
for p being FinSequence of K st p is first-line-of-circulant holds
- p is first-line-of-circulant
proof end;

theorem :: MATRIX16:32
for K being Field
for p being FinSequence of K st p is first-line-of-circulant holds
LCirc (- p) = - (LCirc p)
proof end;

theorem Th33: :: MATRIX16:33
for K being Field
for p, q being FinSequence of K st p is first-line-of-circulant & q is first-line-of-circulant & len p = len q holds
p + q is first-line-of-circulant
proof end;

theorem Th34: :: MATRIX16:34
for K being Field
for p, q being FinSequence of K st len p = len q & p is first-line-of-circulant & q is first-line-of-circulant holds
LCirc (p + q) = (LCirc p) + (LCirc q)
proof end;

theorem Th35: :: MATRIX16:35
for K being Field
for p being FinSequence of K st p is first-col-of-circulant holds
- p is first-col-of-circulant
proof end;

theorem :: MATRIX16:36
for K being Field
for p being FinSequence of K st p is first-col-of-circulant holds
CCirc (- p) = - (CCirc p)
proof end;

theorem Th37: :: MATRIX16:37
for K being Field
for p, q being FinSequence of K st p is first-col-of-circulant & q is first-col-of-circulant & len p = len q holds
p + q is first-col-of-circulant
proof end;

theorem Th38: :: MATRIX16:38
for K being Field
for p, q being FinSequence of K st len p = len q & p is first-col-of-circulant & q is first-col-of-circulant holds
CCirc (p + q) = (CCirc p) + (CCirc q)
proof end;

theorem :: MATRIX16:39
for n being Element of NAT
for K being Field st n > 0 holds
1. (K,n) is col_circulant
proof end;

theorem :: MATRIX16:40
for n being Element of NAT
for K being Field st n > 0 holds
1. (K,n) is line_circulant
proof end;

theorem Th41: :: MATRIX16:41
for K being Field
for a being Element of K
for p being FinSequence of K st p is first-line-of-circulant holds
a * p is first-line-of-circulant
proof end;

theorem Th42: :: MATRIX16:42
for K being Field
for a being Element of K
for p being FinSequence of K st p is first-line-of-circulant holds
LCirc (a * p) = a * (LCirc p)
proof end;

theorem :: MATRIX16:43
for K being Field
for a, b being Element of K
for p being FinSequence of K st p is first-line-of-circulant holds
(a * (LCirc p)) + (b * (LCirc p)) = LCirc ((a + b) * p)
proof end;

theorem :: MATRIX16:44
for K being Field
for a being Element of K
for p, q being FinSequence of K st p is first-line-of-circulant & q is first-line-of-circulant & len p = len q holds
(a * (LCirc p)) + (a * (LCirc q)) = LCirc (a * (p + q))
proof end;

theorem :: MATRIX16:45
for K being Field
for a, b being Element of K
for p, q being FinSequence of K st p is first-line-of-circulant & q is first-line-of-circulant & len p = len q holds
(a * (LCirc p)) + (b * (LCirc q)) = LCirc ((a * p) + (b * q))
proof end;

theorem Th46: :: MATRIX16:46
for K being Field
for a being Element of K
for p being FinSequence of K st p is first-col-of-circulant holds
a * p is first-col-of-circulant
proof end;

theorem Th47: :: MATRIX16:47
for K being Field
for a being Element of K
for p being FinSequence of K st p is first-col-of-circulant holds
CCirc (a * p) = a * (CCirc p)
proof end;

theorem :: MATRIX16:48
for K being Field
for a, b being Element of K
for p being FinSequence of K st p is first-col-of-circulant holds
(a * (CCirc p)) + (b * (CCirc p)) = CCirc ((a + b) * p)
proof end;

theorem :: MATRIX16:49
for K being Field
for a being Element of K
for p, q being FinSequence of K st p is first-col-of-circulant & q is first-col-of-circulant & len p = len q & len p > 0 holds
(a * (CCirc p)) + (a * (CCirc q)) = CCirc (a * (p + q))
proof end;

theorem :: MATRIX16:50
for K being Field
for a, b being Element of K
for p, q being FinSequence of K st p is first-col-of-circulant & q is first-col-of-circulant & len p = len q holds
(a * (CCirc p)) + (b * (CCirc q)) = CCirc ((a * p) + (b * q))
proof end;

notation
let K be set ;
let M be Matrix of K;
synonym circulant M for line_circulant ;
end;

begin

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 :Def9: :: MATRIX16:def 9
( len p = width M1 & ( for i, j being Nat st [i,j] in Indices M1 & i <= j holds
M1 * (i,j) = p . (((j - i) mod (len p)) + 1) ) & ( for i, j being Nat st [i,j] in Indices M1 & i >= j holds
M1 * (i,j) = (- p) . (((j - i) mod (len p)) + 1) ) );
end;

:: deftheorem Def9 defines is_anti-circular_about MATRIX16:def 9 :
for K being Field
for M1 being Matrix of K
for p being FinSequence of K holds
( M1 is_anti-circular_about p iff ( len p = width M1 & ( for i, j being Nat st [i,j] in Indices M1 & i <= j holds
M1 * (i,j) = p . (((j - i) mod (len p)) + 1) ) & ( for i, j being Nat st [i,j] in Indices M1 & i >= j holds
M1 * (i,j) = (- p) . (((j - i) mod (len p)) + 1) ) ) );

definition
let K be Field;
let M be Matrix of K;
attr M is anti-circular means :Def10: :: MATRIX16:def 10
ex p being FinSequence of K st
( len p = width M & M is_anti-circular_about p );
end;

:: deftheorem Def10 defines anti-circular MATRIX16:def 10 :
for K being Field
for M being Matrix of K holds
( M is anti-circular iff ex p being FinSequence of K st
( len p = width M & M is_anti-circular_about p ) );

definition
let K be Field;
let p be FinSequence of K;
attr p is first-line-of-anti-circular means :Def11: :: MATRIX16:def 11
ex M being Matrix of len p,K st M is_anti-circular_about p;
end;

:: deftheorem Def11 defines first-line-of-anti-circular MATRIX16:def 11 :
for K being Field
for p being FinSequence of K holds
( p is first-line-of-anti-circular iff ex M being Matrix of len p,K st M is_anti-circular_about p );

definition
let K be Field;
let p be FinSequence of K;
assume A1: p is first-line-of-anti-circular ;
func ACirc p -> Matrix of len p,K means :Def12: :: MATRIX16:def 12
it is_anti-circular_about p;
existence
ex b1 being Matrix of len p,K st b1 is_anti-circular_about p
by A1, Def11;
uniqueness
for b1, b2 being Matrix of len p,K st b1 is_anti-circular_about p & b2 is_anti-circular_about p holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines ACirc MATRIX16:def 12 :
for K being Field
for p being FinSequence of K st p is first-line-of-anti-circular holds
for b3 being Matrix of len p,K holds
( b3 = ACirc p iff b3 is_anti-circular_about p );

theorem :: MATRIX16:51
for n being Element of NAT
for K being Field
for a being Element of K
for M1 being Matrix of n,K st M1 is anti-circular holds
a * M1 is anti-circular
proof end;

theorem Th52: :: MATRIX16:52
for n being Element of NAT
for K being Field
for M1, M2 being Matrix of n,K st M1 is anti-circular & M2 is anti-circular holds
M1 + M2 is anti-circular
proof end;

theorem :: MATRIX16:53
for K being Fanoian Field
for n, i, j being Nat
for M1 being Matrix of n,K st [i,j] in Indices M1 & i = j & M1 is anti-circular holds
M1 * (i,j) = 0. K
proof end;

theorem :: MATRIX16:54
for i, j, n, k, l being Element of NAT
for K being Field
for M1 being Matrix of n,K st M1 is anti-circular & [i,j] in [:(Seg n),(Seg n):] & k = i + 1 & l = j + 1 & i < n & j < n holds
M1 * (k,l) = M1 * (i,j)
proof end;

theorem Th55: :: MATRIX16:55
for n being Element of NAT
for K being Field
for M1 being Matrix of n,K st M1 is anti-circular holds
- M1 is anti-circular
proof end;

theorem :: MATRIX16:56
for n being Element of NAT
for K being Field
for M1, M2 being Matrix of n,K st M1 is anti-circular & M2 is anti-circular holds
M1 - M2 is anti-circular
proof end;

theorem :: MATRIX16:57
for n being Element of NAT
for K being Field
for p being FinSequence of K
for M1 being Matrix of n,K st M1 is_anti-circular_about p & n > 0 holds
p = Line (M1,1)
proof end;

theorem Th58: :: MATRIX16:58
for K being Field
for p being FinSequence of K st p is first-line-of-anti-circular holds
- p is first-line-of-anti-circular
proof end;

theorem :: MATRIX16:59
for K being Field
for p being FinSequence of K st p is first-line-of-anti-circular holds
ACirc (- p) = - (ACirc p)
proof end;

theorem Th60: :: MATRIX16:60
for K being Field
for p, q being FinSequence of K st p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q holds
p + q is first-line-of-anti-circular
proof end;

theorem Th61: :: MATRIX16:61
for K being Field
for p, q being FinSequence of K st p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q holds
ACirc (p + q) = (ACirc p) + (ACirc q)
proof end;

theorem Th62: :: MATRIX16:62
for K being Field
for a being Element of K
for p being FinSequence of K st p is first-line-of-anti-circular holds
a * p is first-line-of-anti-circular
proof end;

theorem Th63: :: MATRIX16:63
for K being Field
for a being Element of K
for p being FinSequence of K st p is first-line-of-anti-circular holds
ACirc (a * p) = a * (ACirc p)
proof end;

theorem :: MATRIX16:64
for K being Field
for a, b being Element of K
for p being FinSequence of K st p is first-line-of-anti-circular holds
(a * (ACirc p)) + (b * (ACirc p)) = ACirc ((a + b) * p)
proof end;

theorem :: MATRIX16:65
for K being Field
for a being Element of K
for p, q being FinSequence of K st p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q holds
(a * (ACirc p)) + (a * (ACirc q)) = ACirc (a * (p + q))
proof end;

theorem :: MATRIX16:66
for K being Field
for a, b being Element of K
for p, q being FinSequence of K st p is first-line-of-anti-circular & q is first-line-of-anti-circular & len p = len q holds
(a * (ACirc p)) + (b * (ACirc q)) = ACirc ((a * p) + (b * q))
proof end;

registration
let K be Field;
let n be Element of NAT ;
cluster 0. (K,n) -> anti-circular ;
coherence
0. (K,n) is anti-circular
proof end;
end;