mathlib3 documentation

data.matrix.notation

Matrix and vector notation #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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]

meta def matrix.matrix.reflect {α : Type u} {m' : Type u_1} {n' : Type u_2} [reflected_univ] [reflected_univ] [reflected_univ] [reflected (Type u) α] [reflected (Type u_1) m'] [reflected (Type u_2) n'] [h : has_reflect (m' → n' → α)] :

has_reflect (matrix m' n' α)

Matrices can be reflected whenever their entries can. We insert an @id (matrix m' n' α) to prevent immediate decay to a function.

meta def matrix.entry_parser {α : Type} (p : lean.parser α) :

lean.parser (Σ (m n : ℕ), fin m → fin n → α)

Parse the entries of a matrix

@[instance]

meta def matrix.sigma_sigma_fin_matrix_has_reflect {α : Type} [has_reflect α] [reflected Type α] :

has_reflect (Σ (m n : ℕ), fin m → fin n → α)

meta def matrix.notation (_x : interactive.parse (lean.parser.tk "!![")) (val : interactive.parse (matrix.entry_parser (lean.parser.pexpr 1) <* lean.parser.tk "]")) :

lean.parser pexpr

!![a, b; c, d] notation for matrices indexed by fin m and fin n. See the module docstring for details.

@[protected, instance]

def matrix.has_repr {α : Type u} {n m : ℕ} [has_repr α] :

has_repr (matrix (fin m) (fin n) α)

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]

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} (A : matrix m' (fin 0) α) :

A.transpose = ⇑matrix.of matrix.vec_empty

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

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

matrix.vec_head (⇑(matrix.of.symm) A.transpose) = matrix.vec_head ∘ ⇑(matrix.of.symm) A

@[simp]

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

matrix.vec_tail (⇑(matrix.of.symm) A.transpose) = matrix.transpose (matrix.vec_tail ∘ A)

@[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.of matrix.vec_empty

@[simp]

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

A.mul B = 0

@[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 = ⇑matrix.of (λ (_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.of (matrix.vec_tail (⇑(matrix.of.symm) A))).mul 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 : fin m → n' → α) (B : matrix n' o' α) :

(⇑matrix.of (matrix.vec_cons v A)).mul B = ⇑matrix.of (matrix.vec_cons (matrix.vec_mul v B) (⇑(matrix.of.symm) ((⇑matrix.of 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) α) :

matrix.vec_mul v B = matrix.vec_empty

@[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.mul_vec_empty {α : Type u} {m' : Type u_1} [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} [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' → α) :

matrix.vec_mul_vec v w = matrix.vec_empty

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

@[simp]

theorem matrix.submatrix_update_row_succ_above {α : Type u} {m : ℕ} {n' : Type u_2} {o' : Type u_3} (A : matrix (fin m.succ) n' α) (v : n' → α) (f : o' → n') (i : fin m.succ) :

(A.update_row i v).submatrix ⇑(i.succ_above) f = A.submatrix ⇑(i.succ_above) f

Updating a row then removing it is the same as removing it.

@[simp]

theorem matrix.submatrix_update_column_succ_above {α : Type u} {n : ℕ} {m' : Type u_1} {o' : Type u_3} (A : matrix m' (fin n.succ) α) (v : m' → α) (f : o' → m') (i : fin n.succ) :

(A.update_column i v).submatrix f ⇑(i.succ_above) = A.submatrix f ⇑(i.succ_above)

Updating a column then removing it is the same as removing it.

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

1 = ⇑matrix.of ![![1, 0], ![0, 1]]

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

1 = ⇑matrix.of ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]]

theorem matrix.eta_fin_two {α : Type u} (A : matrix (fin 2) (fin 2) α) :

A = ⇑matrix.of ![![A 0 0, A 0 1], ![A 1 0, A 1 1]]

theorem matrix.eta_fin_three {α : Type u} (A : matrix (fin 3) (fin 3) α) :

A = ⇑matrix.of ![![A 0 0, A 0 1, A 0 2], ![A 1 0, A 1 1, A 1 2], ![A 2 0, A 2 1, A 2 2]]

theorem matrix.mul_fin_two {α : Type u} [add_comm_monoid α] [has_mul α] (a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α) :

(⇑matrix.of ![![a₁₁, a₁₂], ![a₂₁, a₂₂]]).mul (⇑matrix.of ![![b₁₁, b₁₂], ![b₂₁, b₂₂]]) = ⇑matrix.of ![![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂], ![a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * 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.vec3_eq {α : Type u} {a₀ a₁ a₂ b₀ b₁ b₂ : α} (h₀ : a₀ = b₀) (h₁ : a₁ = b₁) (h₂ : a₂ = b₂) :

![a₀, a₁, a₂] = ![b₀, b₁, b₂]

theorem matrix.vec2_add {α : Type u} [has_add α] (a₀ a₁ b₀ b₁ : α) :

![a₀, a₁] + ![b₀, b₁] = ![a₀ + b₀, a₁ + b₁]

theorem matrix.vec3_add {α : Type u} [has_add α] (a₀ a₁ a₂ b₀ b₁ b₂ : α) :

![a₀, a₁, a₂] + ![b₀, b₁, b₂] = ![a₀ + b₀, a₁ + b₁, a₂ + b₂]

theorem matrix.smul_vec2 {α : Type u} {R : Type u_1} [has_smul R α] (x : R) (a₀ a₁ : α) :

x • ![a₀, a₁] = ![x • a₀, x • a₁]

theorem matrix.smul_vec3 {α : Type u} {R : Type u_1} [has_smul R α] (x : R) (a₀ a₁ a₂ : α) :

x • ![a₀, a₁, a₂] = ![x • a₀, x • a₁, x • a₂]

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₂ : α} :

matrix.dot_product ![a₀, a₁, a₂] ![b₀, b₁, b₂] = a₀ * b₀ + a₁ * b₁ + a₂ * b₂

@[simp]

theorem matrix.vec3_dot_product {α : Type u} [add_comm_monoid α] [has_mul α] (v w : fin 3 → α) :

matrix.dot_product v w = v 0 * w 0 + v 1 * w 1 + v 2 * w 2