mathlib documentation

data.matrix.notation

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_empty is the empty vector (or 0 by n matrix) ![]
vec_cons prepends an entry to a vector, so ![a, b] is vec_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).

def matrix.vec_empty {α : Type u} :

fin 0 → α

![] is the vector with no entries.

Equations

matrix.vec_empty = fin_zero_elim

def matrix.vec_cons {α : Type u} {n : ℕ} (h : α) (t : fin n → α) :

fin n.succ → α

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

def matrix.vec_head {α : Type u} {n : ℕ} (v : fin n.succ → α) :

α

vec_head v gives the first entry of the vector v

Equations

matrix.vec_head v = v 0

def matrix.vec_tail {α : Type u} {n : ℕ} (v : fin n.succ → α) :

fin n → α

vec_tail v gives a vector consisting of all entries of v except the first

Equations

matrix.vec_tail v = v ∘ fin.succ

theorem matrix.empty_eq {α : Type u} (v : fin 0 → α) :

v = matrix.vec_empty

@[simp]

theorem matrix.head_fin_const {α : Type u} {n : ℕ} (a : α) :

matrix.vec_head (λ (i : fin (n + 1)), a) = a

@[simp]

theorem matrix.cons_val_zero {α : Type u} {m : ℕ} (x : α) (u : fin m → α) :

matrix.vec_cons x u 0 = x

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.cons_val_succ' {α : Type u} {m i : ℕ} (h : i.succ < m.succ) (x : α) (u : fin m → α) :

matrix.vec_cons x u ⟨i.succ, h⟩ = 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.range_cons {α : Type u} {n : ℕ} (x : α) (u : fin n → α) :

set.range (matrix.vec_cons x u) = {x} ∪ set.range u

@[simp]

theorem matrix.range_empty {α : Type u} (u : fin 0 → α) :

set.range 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

### Numeral (bit0 and bit1) indices The following definitions and simp lemmas are to allow any numeral-indexed element of a vector given with matrix notation to be extracted by simp (even when the numeral is larger than the number of elements in the vector, which is taken modulo that number of elements by virtue of the semantics of bit0 and bit1 and of addition on fin n).

@[simp]

theorem matrix.empty_append {α : Type u} {n : ℕ} (v : fin n → α) :

fin.append _ matrix.vec_empty v = v

@[simp]

theorem matrix.cons_append {α : Type u} {m n o : ℕ} (ho : o + 1 = m + 1 + n) (x : α) (u : fin m → α) (v : fin n → α) :

fin.append ho (matrix.vec_cons x u) v = matrix.vec_cons x (fin.append _ u v)

def matrix.vec_alt0 {α : Type u} {m n : ℕ} (hm : m = n + n) (v : fin m → α) (k : fin n) :

α

vec_alt0 v gives a vector with half the length of v, with only alternate elements (even-numbered).

Equations

matrix.vec_alt0 hm v k = v ⟨↑k + ↑k, _⟩

def matrix.vec_alt1 {α : Type u} {m n : ℕ} (hm : m = n + n) (v : fin m → α) (k : fin n) :

α

vec_alt1 v gives a vector with half the length of v, with only alternate elements (odd-numbered).

Equations

matrix.vec_alt1 hm v k = v ⟨↑k + ↑k + 1, _⟩

theorem matrix.vec_alt0_append {α : Type u} {n : ℕ} (v : fin n → α) :

matrix.vec_alt0 rfl (fin.append rfl v v) = v ∘ bit0

theorem matrix.vec_alt1_append {α : Type u} {n : ℕ} (v : fin (n + 1) → α) :

matrix.vec_alt1 rfl (fin.append rfl v v) = v ∘ bit1

@[simp]

theorem matrix.vec_head_vec_alt0 {α : Type u} {m n : ℕ} (hm : m + 2 = n + 1 + (n + 1)) (v : fin (m + 2) → α) :

matrix.vec_head (matrix.vec_alt0 hm v) = v 0

@[simp]

theorem matrix.vec_head_vec_alt1 {α : Type u} {m n : ℕ} (hm : m + 2 = n + 1 + (n + 1)) (v : fin (m + 2) → α) :

matrix.vec_head (matrix.vec_alt1 hm v) = v 1

@[simp]

theorem matrix.cons_vec_bit0_eq_alt0 {α : Type u} {n : ℕ} (x : α) (u : fin n → α) (i : fin (n + 1)) :

matrix.vec_cons x u (bit0 i) = matrix.vec_alt0 rfl (fin.append rfl (matrix.vec_cons x u) (matrix.vec_cons x u)) i

@[simp]

theorem matrix.cons_vec_bit1_eq_alt1 {α : Type u} {n : ℕ} (x : α) (u : fin n → α) (i : fin (n + 1)) :

matrix.vec_cons x u (bit1 i) = matrix.vec_alt1 rfl (fin.append rfl (matrix.vec_cons x u) (matrix.vec_cons x u)) i

@[simp]

theorem matrix.cons_vec_alt0 {α : Type u} {m n : ℕ} (h : m + 1 + 1 = n + 1 + (n + 1)) (x y : α) (u : fin m → α) :

matrix.vec_alt0 h (matrix.vec_cons x (matrix.vec_cons y u)) = matrix.vec_cons x (matrix.vec_alt0 _ u)

@[simp]

theorem matrix.empty_vec_alt0 (α : Type u_1) {h : 0 = 0 + 0} :

matrix.vec_alt0 h matrix.vec_empty = matrix.vec_empty

@[simp]

theorem matrix.cons_vec_alt1 {α : Type u} {m n : ℕ} (h : m + 1 + 1 = n + 1 + (n + 1)) (x y : α) (u : fin m → α) :

matrix.vec_alt1 h (matrix.vec_cons x (matrix.vec_cons y u)) = matrix.vec_cons y (matrix.vec_alt1 _ u)

@[simp]

theorem matrix.empty_vec_alt1 (α : Type u_1) {h : 0 = 0 + 0} :

matrix.vec_alt1 h matrix.vec_empty = matrix.vec_empty

@[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]

theorem matrix.col_empty {α : Type u} (v : fin 0 → α) :

matrix.col v = matrix.vec_empty

@[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) α) :

Aᵀ = matrix.vec_empty

@[simp]

theorem matrix.transpose_empty_cols {α : Type u} {m' : Type u_1} [fintype m'] :

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.vec_cons v A)ᵀ = λ (i : n'), matrix.vec_cons (v i) (Aᵀ i)

@[simp]

theorem matrix.head_transpose {α : Type u} {n : ℕ} {m' : Type u_1} [fintype m'] (A : matrix m' (fin n.succ) α) :

matrix.vec_head Aᵀ = matrix.vec_head ∘ A

@[simp]

theorem matrix.tail_transpose {α : Type u} {n : ℕ} {m' : Type u_1} [fintype m'] (A : matrix m' (fin n.succ) α) :

matrix.vec_tail Aᵀ = (matrix.vec_tail ∘ A)ᵀ

@[simp]

theorem matrix.empty_mul {α : Type u} {n' : Type u_2} {o' : Type u_3} [fintype n'] [fintype o'] [semiring α] (A : matrix (fin 0) n' α) (B : matrix n' o' α) :

A ⬝ B = matrix.vec_empty

@[simp]

theorem matrix.empty_mul_empty {α : Type u} {m' : Type u_1} {o' : Type u_3} [fintype m'] [fintype o'] [semiring α] (A : matrix m' (fin 0) α) (B : matrix (fin 0) o' α) :

A ⬝ B = 0

@[simp]

theorem matrix.mul_empty {α : Type u} {m' : Type u_1} {n' : Type u_2} [fintype m'] [fintype n'] [semiring α] (A : matrix m' n' α) (B : matrix n' (fin 0) α) :

A ⬝ B = λ (_x : m'), matrix.vec_empty

theorem matrix.mul_val_succ {α : Type u} {m : ℕ} {n' : Type u_2} {o' : Type u_3} [fintype n'] [fintype o'] [semiring α] (A : matrix (fin m.succ) n' α) (B : matrix n' o' α) (i : fin m) (j : o') :

(A ⬝ B) i.succ j = (matrix.vec_tail A ⬝ B) i j

@[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.vec_cons v A ⬝ B = matrix.vec_cons (matrix.vec_mul v B) (A ⬝ 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) α) :

matrix.vec_mul v B = matrix.vec_empty

@[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.mul_vec_empty {α : Type u} {m' : Type u_1} [fintype m'] [semiring α] (A : matrix m' (fin 0) α) (v : fin 0 → α) :

A.mul_vec v = 0

@[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' → α) :

matrix.vec_mul_vec v w = matrix.vec_empty

@[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]

theorem matrix.head_add {α : Type u} {n : ℕ} [has_add α] (a b : fin n.succ → α) :

matrix.vec_head (a + b) = matrix.vec_head a + matrix.vec_head b

@[simp]

theorem matrix.tail_add {α : Type u} {n : ℕ} [has_add α] (a b : fin n.succ → α) :

matrix.vec_tail (a + b) = matrix.vec_tail a + matrix.vec_tail b

@[simp]

theorem matrix.empty_sub_empty {α : Type u} [has_sub α] (v w : fin 0 → α) :

v - w = matrix.vec_empty

@[simp]

theorem matrix.cons_sub {α : Type u} {n : ℕ} [has_sub α] (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.sub_cons {α : Type u} {n : ℕ} [has_sub α] (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]

theorem matrix.head_sub {α : Type u} {n : ℕ} [has_sub α] (a b : fin n.succ → α) :

matrix.vec_head (a - b) = matrix.vec_head a - matrix.vec_head b

@[simp]

theorem matrix.tail_sub {α : Type u} {n : ℕ} [has_sub α] (a b : fin n.succ → α) :

matrix.vec_tail (a - b) = matrix.vec_tail a - matrix.vec_tail b

@[simp]

theorem matrix.zero_empty {α : Type u} [has_zero α] :

0 = matrix.vec_empty

@[simp]

theorem matrix.cons_zero_zero {α : Type u} {n : ℕ} [has_zero α] :

matrix.vec_cons 0 0 = 0

@[simp]

theorem matrix.head_zero {α : Type u} {n : ℕ} [has_zero α] :

matrix.vec_head 0 = 0

@[simp]

theorem matrix.tail_zero {α : Type u} {n : ℕ} [has_zero α] :

matrix.vec_tail 0 = 0

@[simp]

theorem matrix.cons_eq_zero_iff {α : Type u} {n : ℕ} [has_zero α] {v : fin n → α} {x : α} :

matrix.vec_cons x v = 0 ↔ x = 0 ∧ v = 0

theorem matrix.cons_nonzero_iff {α : Type u} {n : ℕ} [has_zero α] {v : fin n → α} {x : α} :

matrix.vec_cons x v ≠ 0 ↔ x ≠ 0 ∨ v ≠ 0

@[simp]

theorem matrix.neg_empty {α : Type u} [has_neg α] (v : fin 0 → α) :

-v = matrix.vec_empty

@[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.head_neg {α : Type u} {n : ℕ} [has_neg α] (a : fin n.succ → α) :

matrix.vec_head (-a) = -matrix.vec_head a

@[simp]

theorem matrix.tail_neg {α : Type u} {n : ℕ} [has_neg α] (a : fin n.succ → α) :

matrix.vec_tail (-a) = -matrix.vec_tail a

@[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)