Matrix and vector notation
This file defines notation for vectors and matrices. Given a b c d : α,
the notation allows us to write ![a, b, c, d] : fin 4 → α.
Nesting vectors gives a matrix, so ![![a, b], ![c, d]] : matrix (fin 2) (fin 2) α.
This file includes simp lemmas for applying operations in
data.matrix.basic to values built out of this notation.
Main definitions
vec_emptyis the empty vector (or0bynmatrix)![]vec_consprepends an entry to a vector, so![a, b]isvec_cons a (vec_cons b vec_empty)
Implementation notes
The simp lemmas require that one of the arguments is of the form vec_cons _ _.
This ensures simp works with entries only when (some) entries are already given.
In other words, this notation will only appear in the output of simp if it
already appears in the input.
Notations
The main new notation is ![a, b], which gets expanded to vec_cons a (vec_cons b vec_empty).
![] is the vector with no entries.
Equations
vec_cons h t prepends an entry h to a vector t.
The inverse functions are vec_head and vec_tail.
The notation ![a, b, ...] expands to vec_cons a (vec_cons b ...).
Equations
- matrix.vec_cons h t = fin.cons h t
vec_head v gives the first entry of the vector v
Equations
- matrix.vec_head v = v 0
vec_tail v gives a vector consisting of all entries of v except the first
Equations
- matrix.vec_tail v = v ∘ fin.succ
@[simp]
theorem
matrix.cons_val_zero
{α : Type u}
{m : ℕ}
(x : α)
(u : fin m → α) :
matrix.vec_cons x u 0 = x
@[simp]
theorem
matrix.cons_val_zero'
{α : Type u}
{m : ℕ}
(h : 0 < m.succ)
(x : α)
(u : fin m → α) :
matrix.vec_cons x u ⟨0, h⟩ = x
@[simp]
theorem
matrix.cons_val_succ
{α : Type u}
{m : ℕ}
(x : α)
(u : fin m → α)
(i : fin m) :
matrix.vec_cons x u i.succ = u i
@[simp]
theorem
matrix.head_cons
{α : Type u}
{m : ℕ}
(x : α)
(u : fin m → α) :
matrix.vec_head (matrix.vec_cons x u) = x
@[simp]
theorem
matrix.tail_cons
{α : Type u}
{m : ℕ}
(x : α)
(u : fin m → α) :
matrix.vec_tail (matrix.vec_cons x u) = u
@[simp]
theorem
matrix.empty_val'
{α : Type u}
{n' : Type u_1}
(j : n') :
(λ (i : fin 0), matrix.vec_empty i j) = matrix.vec_empty
@[simp]
theorem
matrix.cons_val'
{α : Type u}
{m : ℕ}
{n' : Type u_2}
[fintype n']
(v : n' → α)
(B : matrix (fin m) n' α)
(i : fin m.succ)
(j : n') :
matrix.vec_cons v B i j = matrix.vec_cons (v j) (λ (i : fin m), B i j) i
@[simp]
theorem
matrix.head_val'
{α : Type u}
{m : ℕ}
{n' : Type u_2}
[fintype n']
(B : matrix (fin m.succ) n' α)
(j : n') :
matrix.vec_head (λ (i : fin m.succ), B i j) = matrix.vec_head B j
@[simp]
theorem
matrix.tail_val'
{α : Type u}
{m : ℕ}
{n' : Type u_2}
[fintype n']
(B : matrix (fin m.succ) n' α)
(j : n') :
matrix.vec_tail (λ (i : fin m.succ), B i j) = λ (i : fin m), matrix.vec_tail B i j
@[simp]
theorem
matrix.cons_head_tail
{α : Type u}
{m : ℕ}
(u : fin m.succ → α) :
matrix.vec_cons (matrix.vec_head u) (matrix.vec_tail u) = u
@[simp]
theorem
matrix.cons_val_one
{α : Type u}
{m : ℕ}
(x : α)
(u : fin m.succ → α) :
matrix.vec_cons x u 1 = matrix.vec_head u
![a, b, ...] 1 is equal to b.
The simplifier needs a special lemma for length ≥ 2, in addition to
cons_val_succ, because 1 : fin 1 = 0 : fin 1.
@[simp]
theorem
matrix.cons_val_fin_one
{α : Type u}
(x : α)
(u : fin 0 → α)
(i : fin 1) :
matrix.vec_cons x u i = x
@[simp]
theorem
matrix.dot_product_empty
{α : Type u}
[add_comm_monoid α]
[has_mul α]
(v w : fin 0 → α) :
matrix.dot_product v w = 0
@[simp]
theorem
matrix.cons_dot_product
{α : Type u}
{n : ℕ}
[add_comm_monoid α]
[has_mul α]
(x : α)
(v : fin n → α)
(w : fin n.succ → α) :
matrix.dot_product (matrix.vec_cons x v) w = x * matrix.vec_head w + matrix.dot_product v (matrix.vec_tail w)
@[simp]
theorem
matrix.dot_product_cons
{α : Type u}
{n : ℕ}
[add_comm_monoid α]
[has_mul α]
(v : fin n.succ → α)
(x : α)
(w : fin n → α) :
matrix.dot_product v (matrix.vec_cons x w) = matrix.vec_head v * x + matrix.dot_product (matrix.vec_tail v) w
@[simp]
@[simp]
theorem
matrix.col_cons
{α : Type u}
{m : ℕ}
(x : α)
(u : fin m → α) :
matrix.col (matrix.vec_cons x u) = matrix.vec_cons (λ (_x : unit), x) (matrix.col u)
@[simp]
theorem
matrix.row_empty
{α : Type u} :
matrix.row matrix.vec_empty = λ (_x : unit), matrix.vec_empty
@[simp]
theorem
matrix.row_cons
{α : Type u}
{m : ℕ}
(x : α)
(u : fin m → α) :
matrix.row (matrix.vec_cons x u) = λ (_x : unit), matrix.vec_cons x u
@[simp]
theorem
matrix.transpose_empty_rows
{α : Type u}
{m' : Type u_1}
[fintype m']
(A : matrix m' (fin 0) α) :
@[simp]
theorem
matrix.transpose_empty_cols
{α : Type u}
{m' : Type u_1}
[fintype m'] :
matrix.transpose matrix.vec_empty = λ (i : m'), matrix.vec_empty
@[simp]
theorem
matrix.cons_transpose
{α : Type u}
{m : ℕ}
{n' : Type u_2}
[fintype n']
(v : n' → α)
(A : matrix (fin m) n' α) :
matrix.transpose (matrix.vec_cons v A) = λ (i : n'), matrix.vec_cons (v i) (A.transpose i)
@[simp]
theorem
matrix.cons_mul
{α : Type u}
{m : ℕ}
{n' : Type u_2}
{o' : Type u_3}
[fintype n']
[fintype o']
[semiring α]
(v : n' → α)
(A : matrix (fin m) n' α)
(B : matrix n' o' α) :
matrix.mul (matrix.vec_cons v A) B = matrix.vec_cons (matrix.vec_mul v B) (A.mul B)
@[simp]
theorem
matrix.empty_vec_mul
{α : Type u}
{o' : Type u_3}
[fintype o']
[semiring α]
(v : fin 0 → α)
(B : matrix (fin 0) o' α) :
matrix.vec_mul v B = 0
@[simp]
theorem
matrix.vec_mul_empty
{α : Type u}
{n' : Type u_2}
[fintype n']
[semiring α]
(v : n' → α)
(B : matrix n' (fin 0) α) :
@[simp]
theorem
matrix.cons_vec_mul
{α : Type u}
{n : ℕ}
{o' : Type u_3}
[fintype o']
[semiring α]
(x : α)
(v : fin n → α)
(B : matrix (fin n.succ) o' α) :
matrix.vec_mul (matrix.vec_cons x v) B = x • matrix.vec_head B + matrix.vec_mul v (matrix.vec_tail B)
@[simp]
theorem
matrix.vec_mul_cons
{α : Type u}
{n : ℕ}
{o' : Type u_3}
[fintype o']
[semiring α]
(v : fin n.succ → α)
(w : o' → α)
(B : matrix (fin n) o' α) :
matrix.vec_mul v (matrix.vec_cons w B) = matrix.vec_head v • w + matrix.vec_mul (matrix.vec_tail v) B
@[simp]
theorem
matrix.empty_mul_vec
{α : Type u}
{n' : Type u_2}
[fintype n']
[semiring α]
(A : matrix (fin 0) n' α)
(v : n' → α) :
A.mul_vec v = matrix.vec_empty
@[simp]
theorem
matrix.cons_mul_vec
{α : Type u}
{m : ℕ}
{n' : Type u_2}
[fintype n']
[semiring α]
(v : n' → α)
(A : fin m → n' → α)
(w : n' → α) :
matrix.mul_vec (matrix.vec_cons v A) w = matrix.vec_cons (matrix.dot_product v w) (matrix.mul_vec A w)
@[simp]
theorem
matrix.mul_vec_cons
{n : ℕ}
{m' : Type u_1}
[fintype m']
{α : Type u_2}
[comm_semiring α]
(A : m' → fin n.succ → α)
(x : α)
(v : fin n → α) :
matrix.mul_vec A (matrix.vec_cons x v) = x • matrix.vec_head ∘ A + matrix.mul_vec (matrix.vec_tail ∘ A) v
@[simp]
theorem
matrix.empty_vec_mul_vec
{α : Type u}
{n' : Type u_2}
[fintype n']
[semiring α]
(v : fin 0 → α)
(w : n' → α) :
@[simp]
theorem
matrix.vec_mul_vec_empty
{α : Type u}
{m' : Type u_1}
[fintype m']
[semiring α]
(v : m' → α)
(w : fin 0 → α) :
matrix.vec_mul_vec v w = λ (_x : m'), matrix.vec_empty
@[simp]
theorem
matrix.cons_vec_mul_vec
{α : Type u}
{m : ℕ}
{n' : Type u_2}
[fintype n']
[semiring α]
(x : α)
(v : fin m → α)
(w : n' → α) :
matrix.vec_mul_vec (matrix.vec_cons x v) w = matrix.vec_cons (x • w) (matrix.vec_mul_vec v w)
@[simp]
theorem
matrix.vec_mul_vec_cons
{α : Type u}
{n : ℕ}
{m' : Type u_1}
[fintype m']
[semiring α]
(v : m' → α)
(x : α)
(w : fin n → α) :
matrix.vec_mul_vec v (matrix.vec_cons x w) = λ (i : m'), v i • matrix.vec_cons x w
@[simp]
theorem
matrix.smul_empty
{α : Type u}
[semiring α]
(x : α)
(v : fin 0 → α) :
x • v = matrix.vec_empty
@[simp]
theorem
matrix.smul_mat_empty
{α : Type u}
[semiring α]
{m' : Type u_1}
(x : α)
(A : fin 0 → m' → α) :
x • A = matrix.vec_empty
@[simp]
theorem
matrix.smul_cons
{α : Type u}
{n : ℕ}
[semiring α]
(x y : α)
(v : fin n → α) :
x • matrix.vec_cons y v = matrix.vec_cons (x * y) (x • v)
@[simp]
theorem
matrix.smul_mat_cons
{α : Type u}
{m : ℕ}
{n' : Type u_2}
[fintype n']
[semiring α]
(x : α)
(v : n' → α)
(A : matrix (fin m) n' α) :
x • matrix.vec_cons v A = matrix.vec_cons (x • v) (x • A)
@[simp]
theorem
matrix.empty_add_empty
{α : Type u}
[has_add α]
(v w : fin 0 → α) :
v + w = matrix.vec_empty
@[simp]
theorem
matrix.cons_add
{α : Type u}
{n : ℕ}
[has_add α]
(x : α)
(v : fin n → α)
(w : fin n.succ → α) :
matrix.vec_cons x v + w = matrix.vec_cons (x + matrix.vec_head w) (v + matrix.vec_tail w)
@[simp]
theorem
matrix.add_cons
{α : Type u}
{n : ℕ}
[has_add α]
(v : fin n.succ → α)
(y : α)
(w : fin n → α) :
v + matrix.vec_cons y w = matrix.vec_cons (matrix.vec_head v + y) (matrix.vec_tail v + w)
@[simp]
@[simp]
@[simp]
theorem
matrix.neg_cons
{α : Type u}
{n : ℕ}
[has_neg α]
(x : α)
(v : fin n → α) :
-matrix.vec_cons x v = matrix.vec_cons (-x) (-v)
@[simp]
theorem
matrix.minor_empty
{α : Type u}
{m' : Type u_1}
{n' : Type u_2}
{o' : Type u_3}
[fintype m']
[fintype n']
[fintype o']
(A : matrix m' n' α)
(row : fin 0 → m')
(col : o' → n') :
A.minor row col = matrix.vec_empty
@[simp]
theorem
matrix.minor_cons_row
{α : Type u}
{m : ℕ}
{m' : Type u_1}
{n' : Type u_2}
{o' : Type u_3}
[fintype m']
[fintype n']
[fintype o']
(A : matrix m' n' α)
(i : m')
(row : fin m → m')
(col : o' → n') :
A.minor (matrix.vec_cons i row) col = matrix.vec_cons (λ (j : o'), A i (col j)) (A.minor row col)