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 bycirculant 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
theorem
Matrix.circulant_col_zero_eq
{α : Type u_1}
{n : Type u_3}
[SubtractionMonoid n]
(v : n → α)
(i : n)
:
theorem
Matrix.Fin.circulant_injective
{α : Type u_1}
(n : ℕ)
:
Function.Injective fun (v : Fin n → α) => circulant v
@[simp]
theorem
Matrix.transpose_circulant
{α : Type u_1}
{n : Type u_3}
[SubtractionMonoid n]
(v : n → α)
:
theorem
Matrix.conjTranspose_circulant
{α : Type u_1}
{n : Type u_3}
[Star α]
[SubtractionMonoid n]
(v : n → α)
:
theorem
Matrix.circulant_mul
{α : Type u_1}
{n : Type u_3}
[NonUnitalNonAssocSemiring α]
[Fintype n]
[AddGroup n]
(v w : n → α)
:
The product of two circulant matrices circulant v
and circulant w
is
the circulant matrix generated by circulant v *ᵥ w
.
theorem
Matrix.circulant_mul_comm
{α : Type u_1}
{n : Type u_3}
[CommMagma α]
[AddCommMonoid α]
[Fintype n]
[AddCommGroup n]
(v w : n → α)
:
Multiplication of circulant matrices commutes when the elements do.
theorem
Matrix.circulant_isSymm_iff
{α : Type u_1}
{n : Type u_3}
[SubtractionMonoid n]
{v : n → α}
:
A circulant of v
is symmetric iff v
equals its reverse.
theorem
Matrix.circulant_isSymm_apply
{α : Type u_1}
{n : Type u_3}
[SubtractionMonoid n]
{v : n → α}
(h : (circulant v).IsSymm)
(i : n)
:
If circulant v
is symmetric, ∀ i j : I, v (- i) = v i
.