Matrix and vector notation #
This file includes simp lemmas for applying operations in data.matrix.basic to values built out
of the matrix notation ![a, b] = vec_cons a (vec_cons b vec_empty) defined in
data.fin.vec_notation.
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 #
We reuse notation ![a, b] for vec_cons a (vec_cons b vec_empty). It is a localized notation in
the matrix locale.
Examples #
Examples of usage can be found in the test/matrix.lean file.
@[protected, instance]
Use ![...] notation for displaying a fin-indexed matrix, for example:
#eval ![![1, 2], ![3, 4]] + ![![3, 4], ![5, 6]] -- ![![4, 6], ![8, 10]]
Equations
@[simp]
theorem
matrix.cons_val'
{α : Type u}
{m : ℕ}
{n' : Type u_2}
(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}
(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}
(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.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.cons_dot_product_cons
{α : Type u}
{n : ℕ}
[add_comm_monoid α]
[has_mul α]
(x : α)
(v : fin n → α)
(y : α)
(w : fin n → α) :
matrix.dot_product (matrix.vec_cons x v) (matrix.vec_cons y w) = x * y + matrix.dot_product 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]
@[simp]
theorem
matrix.transpose_empty_cols
{α : Type u}
{m' : Type u_1} :
matrix.transpose matrix.vec_empty = λ (i : m'), matrix.vec_empty
@[simp]
theorem
matrix.cons_transpose
{α : Type u}
{m : ℕ}
{n' : Type u_2}
(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]
@[simp]
@[simp]
theorem
matrix.empty_mul
{α : Type u}
{n' : Type u_2}
{o' : Type u_3}
[semiring α]
[fintype n']
(A : matrix (fin 0) n' α)
(B : matrix n' o' α) :
A.mul B = matrix.vec_empty
@[simp]
theorem
matrix.mul_empty
{α : Type u}
{m' : Type u_1}
{n' : Type u_2}
[semiring α]
[fintype n']
(A : matrix m' n' α)
(B : matrix n' (fin 0) α) :
A.mul B = λ (_x : m'), matrix.vec_empty
theorem
matrix.mul_val_succ
{α : Type u}
{m : ℕ}
{n' : Type u_2}
{o' : Type u_3}
[semiring α]
[fintype n']
(A : matrix (fin m.succ) n' α)
(B : matrix n' o' α)
(i : fin m)
(j : o') :
A.mul B i.succ j = matrix.mul (matrix.vec_tail A) B i j
@[simp]
theorem
matrix.cons_mul
{α : Type u}
{m : ℕ}
{n' : Type u_2}
{o' : Type u_3}
[semiring α]
[fintype n']
(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}
[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}
[semiring α]
[fintype n']
(v : n' → α)
(B : matrix n' (fin 0) α) :
@[simp]
theorem
matrix.cons_vec_mul
{α : Type u}
{n : ℕ}
{o' : Type u_3}
[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}
[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}
[semiring α]
[fintype n']
(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}
[semiring α]
[fintype n']
(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}
{α : 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}
[semiring α]
(v : fin 0 → α)
(w : n' → α) :
@[simp]
theorem
matrix.vec_mul_vec_empty
{α : Type u}
{m' : Type u_1}
[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}
[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}
[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_mat_empty
{α : Type u}
[semiring α]
{m' : Type u_1}
(x : α)
(A : fin 0 → m' → α) :
x • A = matrix.vec_empty
@[simp]
theorem
matrix.smul_mat_cons
{α : Type u}
{m : ℕ}
{n' : Type u_2}
[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.minor_empty
{α : Type u}
{m' : Type u_1}
{n' : Type u_2}
{o' : Type u_3}
(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}
(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)
theorem
matrix.one_fin_three
{α : Type u}
[has_zero α]
[has_one α] :
1 = ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]]
theorem
matrix.mul_fin_three
{α : Type u}
[add_comm_monoid α]
[has_mul α]
(a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α) :
matrix.mul ![![a₁₁, a₁₂, a₁₃], ![a₂₁, a₂₂, a₂₃], ![a₃₁, a₃₂, a₃₃]] ![![b₁₁, b₁₂, b₁₃], ![b₂₁, b₂₂, b₂₃], ![b₃₁, b₃₂, b₃₃]] = ![![a₁₁ * b₁₁ + a₁₂ * b₂₁ + a₁₃ * b₃₁, a₁₁ * b₁₂ + a₁₂ * b₂₂ + a₁₃ * b₃₂, a₁₁ * b₁₃ + a₁₂ * b₂₃ + a₁₃ * b₃₃], ![a₂₁ * b₁₁ + a₂₂ * b₂₁ + a₂₃ * b₃₁, a₂₁ * b₁₂ + a₂₂ * b₂₂ + a₂₃ * b₃₂, a₂₁ * b₁₃ + a₂₂ * b₂₃ + a₂₃ * b₃₃], ![a₃₁ * b₁₁ + a₃₂ * b₂₁ + a₃₃ * b₃₁, a₃₁ * b₁₂ + a₃₂ * b₂₂ + a₃₃ * b₃₂, a₃₁ * b₁₃ + a₃₂ * b₂₃ + a₃₃ * b₃₃]]
theorem
matrix.vec2_eq
{α : Type u}
{a₀ a₁ b₀ b₁ : α}
(h₀ : a₀ = b₀)
(h₁ : a₁ = b₁) :
![a₀, a₁] = ![b₀, b₁]
theorem
matrix.vec2_dot_product'
{α : Type u}
[add_comm_monoid α]
[has_mul α]
{a₀ a₁ b₀ b₁ : α} :
matrix.dot_product ![a₀, a₁] ![b₀, b₁] = a₀ * b₀ + a₁ * b₁
@[simp]
theorem
matrix.vec2_dot_product
{α : Type u}
[add_comm_monoid α]
[has_mul α]
(v w : fin 2 → α) :
matrix.dot_product v w = v 0 * w 0 + v 1 * w 1
theorem
matrix.vec3_dot_product'
{α : Type u}
[add_comm_monoid α]
[has_mul α]
{a₀ a₁ a₂ b₀ b₁ b₂ : α} :
@[simp]