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 vector v : n → α.
• Matrix.circulant_mul: the product of two circulant matrices circulant v and circulant w is the circulant matrix generated by 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

def Matrix.circulant {α : Type u_1} {n : Type u_4} [Sub n] (v : nα) :
Matrix n n α

Given the condition [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.of fun (i j : n) => v (i - j)
Instances For
@[simp]
theorem Matrix.circulant_apply {α : Type u_1} {n : Type u_4} [Sub n] (v : nα) (i : n) (j : n) :
= v (i - j)
theorem Matrix.circulant_col_zero_eq {α : Type u_1} {n : Type u_4} [] (v : nα) (i : n) :
= v i
theorem Matrix.circulant_injective {α : Type u_1} {n : Type u_4} [] :
Function.Injective Matrix.circulant
theorem Matrix.Fin.circulant_injective {α : Type u_1} (n : ) :
Function.Injective fun (v : Fin nα) =>
@[simp]
theorem Matrix.circulant_inj {α : Type u_1} {n : Type u_4} [] {v : nα} {w : nα} :
v = w
@[simp]
theorem Matrix.Fin.circulant_inj {α : Type u_1} {n : } {v : Fin nα} {w : Fin nα} :
v = w
theorem Matrix.transpose_circulant {α : Type u_1} {n : Type u_4} [] (v : nα) :
().transpose = Matrix.circulant fun (i : n) => v (-i)
theorem Matrix.conjTranspose_circulant {α : Type u_1} {n : Type u_4} [Star α] [] (v : nα) :
().conjTranspose = Matrix.circulant (star fun (i : n) => v (-i))
theorem Matrix.Fin.transpose_circulant {α : Type u_1} {n : } (v : Fin nα) :
().transpose = Matrix.circulant fun (i : Fin n) => v (-i)
theorem Matrix.Fin.conjTranspose_circulant {α : Type u_1} [Star α] {n : } (v : Fin nα) :
().conjTranspose = Matrix.circulant (star fun (i : Fin n) => v (-i))
theorem Matrix.map_circulant {α : Type u_1} {β : Type u_2} {n : Type u_4} [Sub n] (v : nα) (f : αβ) :
().map f = Matrix.circulant fun (i : n) => f (v i)
theorem Matrix.circulant_neg {α : Type u_1} {n : Type u_4} [Neg α] [Sub n] (v : nα) :
@[simp]
theorem Matrix.circulant_zero (α : Type u_6) (n : Type u_7) [Zero α] [Sub n] :
theorem Matrix.circulant_add {α : Type u_1} {n : Type u_4} [Add α] [Sub n] (v : nα) (w : nα) :
theorem Matrix.circulant_sub {α : Type u_1} {n : Type u_4} [Sub α] [Sub n] (v : nα) (w : nα) :
theorem Matrix.circulant_mul {α : Type u_1} {n : Type u_4} [] [] [] (v : nα) (w : nα) :
= Matrix.circulant (().mulVec w)

The product of two circulant matrices circulant v and circulant w is the circulant matrix generated by circulant v *ᵥ w.

theorem Matrix.Fin.circulant_mul {α : Type u_1} [] {n : } (v : Fin nα) (w : Fin nα) :
= Matrix.circulant (().mulVec w)
theorem Matrix.circulant_mul_comm {α : Type u_1} {n : Type u_4} [] [] [] [] (v : nα) (w : nα) :

Multiplication of circulant matrices commutes when the elements do.

theorem Matrix.Fin.circulant_mul_comm {α : Type u_1} [] [] {n : } (v : Fin nα) (w : Fin nα) :
theorem Matrix.circulant_smul {α : Type u_1} {n : Type u_4} {R : Type u_5} [Sub n] [SMul R α] (k : R) (v : nα) :

k • circulant v is another circulant matrix circulant (k • v).

@[simp]
theorem Matrix.circulant_single_one (α : Type u_6) (n : Type u_7) [Zero α] [One α] [] [] :
= 1
@[simp]
theorem Matrix.circulant_single {α : Type u_1} (n : Type u_6) [] [] [] [] (a : α) :
= () a
theorem Matrix.Fin.circulant_ite (α : Type u_6) [Zero α] [One α] (n : ) :
(Matrix.circulant fun (i : Fin n) => if i = 0 then 1 else 0) = 1

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.

theorem Matrix.circulant_isSymm_iff {α : Type u_1} {n : Type u_4} [] {v : nα} :
().IsSymm ∀ (i : n), v (-i) = v i

A circulant of v is symmetric iff v equals its reverse.

theorem Matrix.Fin.circulant_isSymm_iff {α : Type u_1} {n : } {v : Fin nα} :
().IsSymm ∀ (i : Fin n), v (-i) = v i
theorem Matrix.circulant_isSymm_apply {α : Type u_1} {n : Type u_4} [] {v : nα} (h : ().IsSymm) (i : n) :
v (-i) = v i

If circulant v is symmetric, ∀ i j : I, v (- i) = v i.

theorem Matrix.Fin.circulant_isSymm_apply {α : Type u_1} {n : } {v : Fin nα} (h : ().IsSymm) (i : Fin n) :
v (-i) = v i