Documentation

Mathlib.LinearAlgebra.Matrix.Circulant

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 #

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_3} [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
Instances For
    source
    @[simp]
    theorem Matrix.circulant_apply {α : Type u_1} {n : Type u_3} [Sub n] (v : n → α) (i j : n) :
    circulant v i j = v (i - j)
    source
    theorem Matrix.circulant_col_zero_eq {α : Type u_1} {n : Type u_3} [AddGroup n] (v : n → α) (i : n) :
    circulant v i 0 = v i
    source
    theorem Matrix.circulant_injective {α : Type u_1} {n : Type u_3} [AddGroup n] :
    Function.Injective circulant
    source
    theorem Matrix.Fin.circulant_injective {α : Type u_1} (n : ℕ) :
    Function.Injective fun (v : Fin n → α) => circulant v
    source
    @[simp]
    theorem Matrix.circulant_inj {α : Type u_1} {n : Type u_3} [AddGroup n] {v w : n → α} :
    circulant v = circulant w ↔ v = w
    source
    @[simp]
    theorem Matrix.Fin.circulant_inj {α : Type u_1} {n : ℕ} {v w : Fin n → α} :
    circulant v = circulant w ↔ v = w
    source
    theorem Matrix.transpose_circulant {α : Type u_1} {n : Type u_3} [AddGroup n] (v : n → α) :
    (circulant v).transpose = circulant fun (i : n) => v (-i)
    source
    theorem Matrix.conjTranspose_circulant {α : Type u_1} {n : Type u_3} [Star α] [AddGroup n] (v : n → α) :
    (circulant v).conjTranspose = circulant (star fun (i : n) => v (-i))
    source
    theorem Matrix.Fin.transpose_circulant {α : Type u_1} {n : ℕ} (v : Fin n → α) :
    (circulant v).transpose = circulant fun (i : Fin n) => v (-i)
    source
    theorem Matrix.Fin.conjTranspose_circulant {α : Type u_1} [Star α] {n : ℕ} (v : Fin n → α) :
    (circulant v).conjTranspose = circulant (star fun (i : Fin n) => v (-i))
    source
    theorem Matrix.map_circulant {α : Type u_1} {β : Type u_2} {n : Type u_3} [Sub n] (v : n → α) (f : α → β) :
    (circulant v).map f = circulant fun (i : n) => f (v i)
    source
    theorem Matrix.circulant_neg {α : Type u_1} {n : Type u_3} [Neg α] [Sub n] (v : n → α) :
    circulant (-v) = -circulant v
    source
    @[simp]
    theorem Matrix.circulant_zero (α : Type u_5) (n : Type u_6) [Zero α] [Sub n] :
    circulant 0 = 0
    source
    theorem Matrix.circulant_add {α : Type u_1} {n : Type u_3} [Add α] [Sub n] (v w : n → α) :
    circulant (v + w) = circulant v + circulant w
    source
    theorem Matrix.circulant_sub {α : Type u_1} {n : Type u_3} [Sub α] [Sub n] (v w : n → α) :
    circulant (v - w) = circulant v - circulant w
    source
    theorem Matrix.circulant_mul {α : Type u_1} {n : Type u_3} [Semiring α] [Fintype n] [AddGroup n] (v w : n → α) :
    circulant v * circulant w = circulant ((circulant v).mulVec w)

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

    source
    theorem Matrix.Fin.circulant_mul {α : Type u_1} [Semiring α] {n : ℕ} (v w : Fin n → α) :
    circulant v * circulant w = circulant ((circulant v).mulVec w)
    source
    theorem Matrix.circulant_mul_comm {α : Type u_1} {n : Type u_3} [CommSemigroup α] [AddCommMonoid α] [Fintype n] [AddCommGroup n] (v w : n → α) :
    circulant v * circulant w = circulant w * circulant v

    Multiplication of circulant matrices commutes when the elements do.

    source
    theorem Matrix.Fin.circulant_mul_comm {α : Type u_1} [CommSemigroup α] [AddCommMonoid α] {n : ℕ} (v w : Fin n → α) :
    circulant v * circulant w = circulant w * circulant v
    source
    theorem Matrix.circulant_smul {α : Type u_1} {n : Type u_3} {R : Type u_4} [Sub n] [SMul R α] (k : R) (v : n → α) :
    circulant (k • v) = k • circulant v

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

    source
    @[simp]
    theorem Matrix.circulant_single_one (α : Type u_5) (n : Type u_6) [Zero α] [One α] [DecidableEq n] [AddGroup n] :
    circulant (Pi.single 0 1) = 1
    source
    @[simp]
    theorem Matrix.circulant_single {α : Type u_1} (n : Type u_5) [Semiring α] [DecidableEq n] [AddGroup n] [Fintype n] (a : α) :
    circulant (Pi.single 0 a) = (scalar n) a
    source
    theorem Matrix.Fin.circulant_ite (α : Type u_5) [Zero α] [One α] (n : ℕ) :
    (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.

    source
    theorem Matrix.circulant_isSymm_iff {α : Type u_1} {n : Type u_3} [AddGroup n] {v : n → α} :
    (circulant v).IsSymm ↔ ∀ (i : n), v (-i) = v i

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

    source
    theorem Matrix.Fin.circulant_isSymm_iff {α : Type u_1} {n : ℕ} {v : Fin n → α} :
    (circulant v).IsSymm ↔ ∀ (i : Fin n), v (-i) = v i
    source
    theorem Matrix.circulant_isSymm_apply {α : Type u_1} {n : Type u_3} [AddGroup n] {v : n → α} (h : (circulant v).IsSymm) (i : n) :
    v (-i) = v i

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

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