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.
This also provides the new notation !![a, b; c, d] = matrix.of ![![a, b], ![c, d]].
This notation also works for empty matrices; !![,,,] : matrix (fin 0) (fin 3) and
!![;;;] : matrix (fin 3) (fin 0).
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 #
This file provide notation !![a, b; c, d] for matrices, which corresponds to
matrix.of ![![a, b], ![c, d]].
A parser for a, b; c, d-style strings is provided as matrix.entry_parser, while
matrix.notation provides the hook for the !! notation.
Note that in lean 3 the pretty-printer will not show !! notation, instead showing the version
with of ![![...]].
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
- matrix.has_repr = {repr := λ (f : matrix (fin m) (fin n) α), "!![" ++ "; ".intercalate (list.map (λ (i : fin m), ", ".intercalate (list.map (λ (j : fin n), repr (f i j)) (list.fin_range n))) (list.fin_range m)) ++ "]"}
@[simp]
theorem
matrix.cons_val'
{α : Type u}
{m : ℕ}
{n' : Type u_2}
(v : n' → α)
(B : 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 : 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 : 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}
(A : matrix (fin 0) m' α) :
A.transpose = ⇑matrix.of (λ (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.of (matrix.vec_cons v A)).transpose = ⇑matrix.of (λ (i : n'), matrix.vec_cons (v i) (A.transpose i))
@[simp]
@[simp]
@[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 : fin n.succ → o' → α) :
matrix.vec_mul (matrix.vec_cons x v) (⇑matrix.of B) = x • matrix.vec_head B + matrix.vec_mul v (⇑matrix.of (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 : fin n → o' → α) :
matrix.vec_mul v (⇑matrix.of (matrix.vec_cons w B)) = matrix.vec_head v • w + matrix.vec_mul (matrix.vec_tail v) (⇑matrix.of B)
@[simp]
theorem
matrix.cons_vec_mul_cons
{α : Type u}
{n : ℕ}
{o' : Type u_3}
[semiring α]
(x : α)
(v : fin n → α)
(w : o' → α)
(B : fin n → o' → α) :
matrix.vec_mul (matrix.vec_cons x v) (⇑matrix.of (matrix.vec_cons w B)) = x • w + matrix.vec_mul v (⇑matrix.of 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.of (matrix.vec_cons v A)).mul_vec w = matrix.vec_cons (matrix.dot_product v w) ((⇑matrix.of A).mul_vec 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.of A).mul_vec (matrix.vec_cons x v) = x • matrix.vec_head ∘ A + (⇑matrix.of (matrix.vec_tail ∘ A)).mul_vec 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 : fin m → n' → α) :
x • matrix.vec_cons v A = matrix.vec_cons (x • v) (x • A)
@[simp]
theorem
matrix.submatrix_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.submatrix row col = matrix.vec_empty
@[simp]
theorem
matrix.submatrix_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.submatrix (matrix.vec_cons i row) col = matrix.vec_cons (λ (j : o'), A i (col j)) (A.submatrix row col)
theorem
matrix.mul_fin_two
{α : Type u}
[add_comm_monoid α]
[has_mul α]
(a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α) :
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.of ![![a₁₁, a₁₂, a₁₃], ![a₂₁, a₂₂, a₂₃], ![a₃₁, a₃₂, a₃₃]]).mul (⇑matrix.of ![![b₁₁, b₁₂, b₁₃], ![b₂₁, b₂₂, b₂₃], ![b₃₁, b₃₂, b₃₃]]) = ⇑matrix.of ![![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]