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]