mathlib3 documentation

linear_algebra.matrix.circulant

Circulant matrices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

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

source
def matrix.circulant {α : Type u_1} {n : Type u_4} [has_sub n] (v : n → α) :
matrix n n α

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
source
@[simp]
theorem matrix.circulant_apply {α : Type u_1} {n : Type u_4} [has_sub n] (v : n → α) (i j : n) :
matrix.circulant v i j = v (i - j)
source
theorem matrix.circulant_col_zero_eq {α : Type u_1} {n : Type u_4} [add_group n] (v : n → α) (i : n) :
matrix.circulant v i 0 = v i
source
theorem matrix.circulant_injective {α : Type u_1} {n : Type u_4} [add_group n] :
function.injective matrix.circulant
source
theorem matrix.fin.circulant_injective {α : Type u_1} (n : ℕ) :
function.injective (λ (v : fin n → α), matrix.circulant v)
source
@[simp]
theorem matrix.circulant_inj {α : Type u_1} {n : Type u_4} [add_group n] {v w : n → α} :
matrix.circulant v = matrix.circulant w ↔ v = w
source
@[simp]
theorem matrix.fin.circulant_inj {α : Type u_1} {n : ℕ} {v w : fin n → α} :
matrix.circulant v = matrix.circulant w ↔ v = w
source
theorem matrix.transpose_circulant {α : Type u_1} {n : Type u_4} [add_group n] (v : n → α) :
(matrix.circulant v).transpose = matrix.circulant (λ (i : n), v (-i))
source
theorem matrix.conj_transpose_circulant {α : Type u_1} {n : Type u_4} [has_star α] [add_group n] (v : n → α) :
(matrix.circulant v).conj_transpose = matrix.circulant (has_star.star (λ (i : n), v (-i)))
source
theorem matrix.fin.transpose_circulant {α : Type u_1} {n : ℕ} (v : fin n → α) :
(matrix.circulant v).transpose = matrix.circulant (λ (i : fin n), v (-i))
source
theorem matrix.fin.conj_transpose_circulant {α : Type u_1} [has_star α] {n : ℕ} (v : fin n → α) :
(matrix.circulant v).conj_transpose = matrix.circulant (has_star.star (λ (i : fin n), v (-i)))
source
theorem matrix.map_circulant {α : Type u_1} {β : Type u_2} {n : Type u_4} [has_sub n] (v : n → α) (f : α → β) :
(matrix.circulant v).map f = matrix.circulant (λ (i : n), f (v i))
source
theorem matrix.circulant_neg {α : Type u_1} {n : Type u_4} [has_neg α] [has_sub n] (v : n → α) :
matrix.circulant (-v) = -matrix.circulant v
source
@[simp]
theorem matrix.circulant_zero (α : Type u_1) (n : Type u_2) [has_zero α] [has_sub n] :
matrix.circulant 0 = 0
source
theorem matrix.circulant_add {α : Type u_1} {n : Type u_4} [has_add α] [has_sub n] (v w : n → α) :
matrix.circulant (v + w) = matrix.circulant v + matrix.circulant w
source
theorem matrix.circulant_sub {α : Type u_1} {n : Type u_4} [has_sub α] [has_sub n] (v w : n → α) :
matrix.circulant (v - w) = matrix.circulant v - matrix.circulant w
source
theorem matrix.circulant_mul {α : Type u_1} {n : Type u_4} [semiring α] [fintype n] [add_group n] (v w : n → α) :
(matrix.circulant v).mul (matrix.circulant w) = matrix.circulant ((matrix.circulant v).mul_vec w)

The product of two circulant matrices circulant v and circulant w is the circulant matrix generated by mul_vec (circulant v) w.

source
theorem matrix.fin.circulant_mul {α : Type u_1} [semiring α] {n : ℕ} (v w : fin n → α) :
(matrix.circulant v).mul (matrix.circulant w) = matrix.circulant ((matrix.circulant v).mul_vec w)
source
theorem matrix.circulant_mul_comm {α : Type u_1} {n : Type u_4} [comm_semigroup α] [add_comm_monoid α] [fintype n] [add_comm_group n] (v w : n → α) :
(matrix.circulant v).mul (matrix.circulant w) = (matrix.circulant w).mul (matrix.circulant v)

Multiplication of circulant matrices commutes when the elements do.

source
theorem matrix.fin.circulant_mul_comm {α : Type u_1} [comm_semigroup α] [add_comm_monoid α] {n : ℕ} (v w : fin n → α) :
(matrix.circulant v).mul (matrix.circulant w) = (matrix.circulant w).mul (matrix.circulant v)
source
theorem matrix.circulant_smul {α : Type u_1} {n : Type u_4} {R : Type u_5} [has_sub n] [has_smul R α] (k : R) (v : n → α) :
matrix.circulant (k • v) = k • matrix.circulant v

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

source
@[simp]
theorem matrix.circulant_single_one (α : Type u_1) (n : Type u_2) [has_zero α] [has_one α] [decidable_eq n] [add_group n] :
matrix.circulant (pi.single 0 1) = 1
source
@[simp]
theorem matrix.circulant_single {α : Type u_1} (n : Type u_2) [semiring α] [decidable_eq n] [add_group n] [fintype n] (a : α) :
matrix.circulant (pi.single 0 a) = ⇑(matrix.scalar n) a
source
theorem matrix.fin.circulant_ite (α : Type u_1) [has_zero α] [has_one α] (n : ℕ) :
matrix.circulant (λ (i : fin n), ite (↑i = 0) 1 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.

source
theorem matrix.circulant_is_symm_iff {α : Type u_1} {n : Type u_4} [add_group n] {v : n → α} :
(matrix.circulant v).is_symm ↔ ∀ (i : n), v (-i) = v i

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

source
theorem matrix.fin.circulant_is_symm_iff {α : Type u_1} {n : ℕ} {v : fin n → α} :
(matrix.circulant v).is_symm ↔ ∀ (i : fin n), v (-i) = v i
source
theorem matrix.circulant_is_symm_apply {α : Type u_1} {n : Type u_4} [add_group n] {v : n → α} (h : (matrix.circulant v).is_symm) (i : n) :
v (-i) = v i

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

source
theorem matrix.fin.circulant_is_symm_apply {α : Type u_1} {n : ℕ} {v : fin n → α} (h : (matrix.circulant v).is_symm) (i : fin n) :
v (-i) = v i