Circulant matrices #
This file contains the definition and basic results about circulant matrices.
Given a vector v : n → α
indexed by a type that is endowed with subtraction,
matrix.circulant v
is the matrix whose (i, j)
th entry is v (i - j)
.
Main results #
matrix.circulant
: the circulant matrix generated by a given vectorv : n → α
.matrix.circulant_mul
: the product of two circulant matricescirculant v
andcirculant w
is the circulant matrix generated bymul_vec (circulant v) w
.matrix.circulant_mul_comm
: multiplication of circulant matrices commutes when the elements do.
Implementation notes #
matrix.fin.foo
is the fin n
version of matrix.foo
.
Namely, the index type of the circulant matrices in discussion is fin n
.
Tags #
circulant, matrix
Given the condition [has_sub n]
and a vector v : n → α
,
we define circulant v
to be the circulant matrix generated by v
of type matrix n n α
.
The (i,j)
th entry is defined to be v (i - j)
.
Equations
- matrix.circulant v i j = v (i - j)
The product of two circulant matrices circulant v
and circulant w
is
the circulant matrix generated by mul_vec (circulant v) w
.
Multiplication of circulant matrices commutes when the elements do.
k • circulant v
is another circulant matrix circulant (k • v)
.
Note we use ↑i = 0
instead of i = 0
as fin 0
has no 0
.
This means that we cannot state this with pi.single
as we did with matrix.circulant_single
.
If circulant v
is symmetric, ∀ i j : I, v (- i) = v i
.