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] = vecCons a (vecCons b vecEmpty) defined in Data.Fin.VecNotation.

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 vecCons _ _. 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]]. TODO: until we implement a Lean.PrettyPrinter.Unexpander for Matrix.of, 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.

instance Matrix.toExpr {α : Type u} {m' : Type uₘ} {n' : Type uₙ} [Lean.ToLevel.{u}] [Lean.ToLevel.{uₘ}] [Lean.ToLevel.{uₙ}] [Lean.ToExpr α] [Lean.ToExpr m'] [Lean.ToExpr n'] [Lean.ToExpr (m' → n' → α)] : Lean.ToExpr (Matrix m' n' α)

Matrices can be reflected whenever their entries can. We insert a Matrix.of to prevent immediate decay to a function.

Equations

• One or more equations did not get rendered due to their size.

def Matrix.matrixNotation : Lean.ParserDescr

Notation for m×n matrices, aka Matrix (Fin m) (Fin n) α.

For instance:

• !![a, b, c; d, e, f] is the matrix with two rows and three columns, of type Matrix (Fin 2) (Fin 3) α
• !![a, b, c] is a row vector of type Matrix (Fin 1) (Fin 3) α (see also Matrix.row).
• !![a; b; c] is a column vector of type Matrix (Fin 3) (Fin 1) α (see also Matrix.col).

This notation implements some special cases:

• ![,,], with n ,s, is a term of type Matrix (Fin 0) (Fin n) α
• ![;;], with m ;s, is a term of type Matrix (Fin m) (Fin 0) α
• ![] is the 0×0 matrix

Note that vector notation is provided elsewhere (by Matrix.vecNotation) as ![a, b, c]. Under the hood, !![a, b, c; d, e, f] is syntax for Matrix.of ![![a, b, c], ![d, e, f]].

Equations

• One or more equations did not get rendered due to their size.

def Matrix.matrixNotationRx0 : Lean.ParserDescr

Notation for m×n matrices, aka Matrix (Fin m) (Fin n) α.

For instance:

• !![a, b, c; d, e, f] is the matrix with two rows and three columns, of type Matrix (Fin 2) (Fin 3) α
• !![a, b, c] is a row vector of type Matrix (Fin 1) (Fin 3) α (see also Matrix.row).
• !![a; b; c] is a column vector of type Matrix (Fin 3) (Fin 1) α (see also Matrix.col).

This notation implements some special cases:

• ![,,], with n ,s, is a term of type Matrix (Fin 0) (Fin n) α
• ![;;], with m ;s, is a term of type Matrix (Fin m) (Fin 0) α
• ![] is the 0×0 matrix

Note that vector notation is provided elsewhere (by Matrix.vecNotation) as ![a, b, c]. Under the hood, !![a, b, c; d, e, f] is syntax for Matrix.of ![![a, b, c], ![d, e, f]].

Equations

• One or more equations did not get rendered due to their size.

def Matrix.matrixNotation0xC : Lean.ParserDescr

Notation for m×n matrices, aka Matrix (Fin m) (Fin n) α.

For instance:

• !![a, b, c; d, e, f] is the matrix with two rows and three columns, of type Matrix (Fin 2) (Fin 3) α
• !![a, b, c] is a row vector of type Matrix (Fin 1) (Fin 3) α (see also Matrix.row).
• !![a; b; c] is a column vector of type Matrix (Fin 3) (Fin 1) α (see also Matrix.col).

This notation implements some special cases:

• ![,,], with n ,s, is a term of type Matrix (Fin 0) (Fin n) α
• ![;;], with m ;s, is a term of type Matrix (Fin m) (Fin 0) α
• ![] is the 0×0 matrix

Note that vector notation is provided elsewhere (by Matrix.vecNotation) as ![a, b, c]. Under the hood, !![a, b, c; d, e, f] is syntax for Matrix.of ![![a, b, c], ![d, e, f]].

Equations

• One or more equations did not get rendered due to their size.

instance Matrix.repr {α : Type u} {n : ℕ} {m : ℕ} [Repr α] : 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

• One or more equations did not get rendered due to their size.

@[simp]

theorem Matrix.cons_val' {α : Type u} {m : ℕ} {n' : Type uₙ} (v : n' → α) (B : Fin m → n' → α) (i : Fin m.succ) (j : n') : Matrix.vecCons v B i j = Matrix.vecCons (v j) (fun (i : Fin m) => B i j) i

@[simp]

theorem Matrix.head_val' {α : Type u} {m : ℕ} {n' : Type uₙ} (B : Fin m.succ → n' → α) (j : n') : (Matrix.vecHead fun (i : Fin m.succ) => B i j) = Matrix.vecHead B j

@[simp]

theorem Matrix.tail_val' {α : Type u} {m : ℕ} {n' : Type uₙ} (B : Fin m.succ → n' → α) (j : n') : (Matrix.vecTail fun (i : Fin m.succ) => B i j) = fun (i : Fin m) => Matrix.vecTail B i j

@[simp]

theorem Matrix.dotProduct_empty {α : Type u} [AddCommMonoid α] [Mul α] (v : Fin 0 → α) (w : Fin 0 → α) : Matrix.dotProduct v w = 0

@[simp]

theorem Matrix.cons_dotProduct {α : Type u} {n : ℕ} [AddCommMonoid α] [Mul α] (x : α) (v : Fin n → α) (w : Fin n.succ → α) : Matrix.dotProduct (Matrix.vecCons x v) w = x * Matrix.vecHead w + Matrix.dotProduct v (Matrix.vecTail w)

@[simp]

theorem Matrix.dotProduct_cons {α : Type u} {n : ℕ} [AddCommMonoid α] [Mul α] (v : Fin n.succ → α) (x : α) (w : Fin n → α) : Matrix.dotProduct v (Matrix.vecCons x w) = Matrix.vecHead v * x + Matrix.dotProduct (Matrix.vecTail v) w

theorem Matrix.cons_dotProduct_cons {α : Type u} {n : ℕ} [AddCommMonoid α] [Mul α] (x : α) (v : Fin n → α) (y : α) (w : Fin n → α) : Matrix.dotProduct (Matrix.vecCons x v) (Matrix.vecCons y w) = x * y + Matrix.dotProduct v w

@[simp]

theorem Matrix.col_empty {α : Type u} {ι : Type u_1} (v : Fin 0 → α) : Matrix.col ι v = ![]

@[simp]

theorem Matrix.col_cons {α : Type u} {m : ℕ} {ι : Type u_1} (x : α) (u : Fin m → α) : Matrix.col ι (Matrix.vecCons x u) = Matrix.of (Matrix.vecCons (fun (x_1 : ι) => x) (Matrix.col ι u))

@[simp]

theorem Matrix.row_empty {α : Type u} {ι : Type u_1} : Matrix.row ι ![] = Matrix.of fun (x : ι) => ![]

@[simp]

theorem Matrix.row_cons {α : Type u} {m : ℕ} {ι : Type u_1} (x : α) (u : Fin m → α) : Matrix.row ι (Matrix.vecCons x u) = Matrix.of fun (x_1 : ι) => Matrix.vecCons x u

@[simp]

theorem Matrix.transpose_empty_rows {α : Type u} {m' : Type uₘ} (A : Matrix m' (Fin 0) α) : A.transpose = Matrix.of ![]

@[simp]

theorem Matrix.transpose_empty_cols {α : Type u} {m' : Type uₘ} (A : Matrix (Fin 0) m' α) : A.transpose = Matrix.of fun (x : m') => ![]

@[simp]

theorem Matrix.cons_transpose {α : Type u} {m : ℕ} {n' : Type uₙ} (v : n' → α) (A : Matrix (Fin m) n' α) : (Matrix.of (Matrix.vecCons v A)).transpose = Matrix.of fun (i : n') => Matrix.vecCons (v i) (A.transpose i)

@[simp]

theorem Matrix.head_transpose {α : Type u} {n : ℕ} {m' : Type uₘ} (A : Matrix m' (Fin n.succ) α) : Matrix.vecHead (Matrix.of.symm A.transpose) = Matrix.vecHead ∘ Matrix.of.symm A

@[simp]

theorem Matrix.tail_transpose {α : Type u} {n : ℕ} {m' : Type uₘ} (A : Matrix m' (Fin n.succ) α) : Matrix.vecTail (Matrix.of.symm A.transpose) = Matrix.transpose (Matrix.vecTail ∘ A)

@[simp]

theorem Matrix.empty_mul {α : Type u} {n' : Type uₙ} {o' : Type uₒ} [NonUnitalNonAssocSemiring α] [Fintype n'] (A : Matrix (Fin 0) n' α) (B : Matrix n' o' α) : A * B = Matrix.of ![]

@[simp]

theorem Matrix.empty_mul_empty {α : Type u} {m' : Type uₘ} {o' : Type uₒ} [NonUnitalNonAssocSemiring α] (A : Matrix m' (Fin 0) α) (B : Matrix (Fin 0) o' α) : A * B = 0

@[simp]

theorem Matrix.mul_empty {α : Type u} {m' : Type uₘ} {n' : Type uₙ} [NonUnitalNonAssocSemiring α] [Fintype n'] (A : Matrix m' n' α) (B : Matrix n' (Fin 0) α) : A * B = Matrix.of fun (x : m') => ![]

theorem Matrix.mul_val_succ {α : Type u} {m : ℕ} {n' : Type uₙ} {o' : Type uₒ} [NonUnitalNonAssocSemiring α] [Fintype n'] (A : Matrix (Fin m.succ) n' α) (B : Matrix n' o' α) (i : Fin m) (j : o') : (A * B) i.succ j = (Matrix.of (Matrix.vecTail (Matrix.of.symm A)) * B) i j

@[simp]

theorem Matrix.cons_mul {α : Type u} {m : ℕ} {n' : Type uₙ} {o' : Type uₒ} [NonUnitalNonAssocSemiring α] [Fintype n'] (v : n' → α) (A : Fin m → n' → α) (B : Matrix n' o' α) : Matrix.of (Matrix.vecCons v A) * B = Matrix.of (Matrix.vecCons (Matrix.vecMul v B) (Matrix.of.symm (Matrix.of A * B)))

@[simp]

theorem Matrix.empty_vecMul {α : Type u} {o' : Type uₒ} [NonUnitalNonAssocSemiring α] (v : Fin 0 → α) (B : Matrix (Fin 0) o' α) : Matrix.vecMul v B = 0

@[simp]

theorem Matrix.vecMul_empty {α : Type u} {n' : Type uₙ} [NonUnitalNonAssocSemiring α] [Fintype n'] (v : n' → α) (B : Matrix n' (Fin 0) α) : Matrix.vecMul v B = ![]

@[simp]

theorem Matrix.cons_vecMul {α : Type u} {n : ℕ} {o' : Type uₒ} [NonUnitalNonAssocSemiring α] (x : α) (v : Fin n → α) (B : Fin n.succ → o' → α) : Matrix.vecMul (Matrix.vecCons x v) (Matrix.of B) = x • Matrix.vecHead B + Matrix.vecMul v (Matrix.of (Matrix.vecTail B))

@[simp]

theorem Matrix.vecMul_cons {α : Type u} {n : ℕ} {o' : Type uₒ} [NonUnitalNonAssocSemiring α] (v : Fin n.succ → α) (w : o' → α) (B : Fin n → o' → α) : Matrix.vecMul v (Matrix.of (Matrix.vecCons w B)) = Matrix.vecHead v • w + Matrix.vecMul (Matrix.vecTail v) (Matrix.of B)

theorem Matrix.cons_vecMul_cons {α : Type u} {n : ℕ} {o' : Type uₒ} [NonUnitalNonAssocSemiring α] (x : α) (v : Fin n → α) (w : o' → α) (B : Fin n → o' → α) : Matrix.vecMul (Matrix.vecCons x v) (Matrix.of (Matrix.vecCons w B)) = x • w + Matrix.vecMul v (Matrix.of B)

@[simp]

theorem Matrix.empty_mulVec {α : Type u} {n' : Type uₙ} [NonUnitalNonAssocSemiring α] [Fintype n'] (A : Matrix (Fin 0) n' α) (v : n' → α) : A.mulVec v = ![]

@[simp]

theorem Matrix.mulVec_empty {α : Type u} {m' : Type uₘ} [NonUnitalNonAssocSemiring α] (A : Matrix m' (Fin 0) α) (v : Fin 0 → α) : A.mulVec v = 0

@[simp]

theorem Matrix.cons_mulVec {α : Type u} {m : ℕ} {n' : Type uₙ} [NonUnitalNonAssocSemiring α] [Fintype n'] (v : n' → α) (A : Fin m → n' → α) (w : n' → α) : (Matrix.of (Matrix.vecCons v A)).mulVec w = Matrix.vecCons (Matrix.dotProduct v w) ((Matrix.of A).mulVec w)

@[simp]

theorem Matrix.mulVec_cons {n : ℕ} {m' : Type uₘ} {α : Type u_1} [CommSemiring α] (A : m' → Fin n.succ → α) (x : α) (v : Fin n → α) : (Matrix.of A).mulVec (Matrix.vecCons x v) = x • Matrix.vecHead ∘ A + (Matrix.of (Matrix.vecTail ∘ A)).mulVec v

@[simp]

theorem Matrix.empty_vecMulVec {α : Type u} {n' : Type uₙ} [NonUnitalNonAssocSemiring α] (v : Fin 0 → α) (w : n' → α) : Matrix.vecMulVec v w = ![]

@[simp]

theorem Matrix.vecMulVec_empty {α : Type u} {m' : Type uₘ} [NonUnitalNonAssocSemiring α] (v : m' → α) (w : Fin 0 → α) : Matrix.vecMulVec v w = Matrix.of fun (x : m') => ![]

@[simp]

theorem Matrix.cons_vecMulVec {α : Type u} {m : ℕ} {n' : Type uₙ} [NonUnitalNonAssocSemiring α] (x : α) (v : Fin m → α) (w : n' → α) : Matrix.vecMulVec (Matrix.vecCons x v) w = Matrix.vecCons (x • w) (Matrix.vecMulVec v w)

@[simp]

theorem Matrix.vecMulVec_cons {α : Type u} {n : ℕ} {m' : Type uₘ} [NonUnitalNonAssocSemiring α] (v : m' → α) (x : α) (w : Fin n → α) : Matrix.vecMulVec v (Matrix.vecCons x w) = Matrix.of fun (i : m') => v i • Matrix.vecCons x w

theorem Matrix.smul_mat_empty {α : Type u} [NonUnitalNonAssocSemiring α] {m' : Type u_1} (x : α) (A : Fin 0 → m' → α) : x • A = ![]

theorem Matrix.smul_mat_cons {α : Type u} {m : ℕ} {n' : Type uₙ} [NonUnitalNonAssocSemiring α] (x : α) (v : n' → α) (A : Fin m → n' → α) : x • Matrix.vecCons v A = Matrix.vecCons (x • v) (x • A)

@[simp]

theorem Matrix.submatrix_empty {α : Type u} {m' : Type uₘ} {n' : Type uₙ} {o' : Type uₒ} (A : Matrix m' n' α) (row : Fin 0 → m') (col : o' → n') : A.submatrix row col = ![]

@[simp]

theorem Matrix.submatrix_cons_row {α : Type u} {m : ℕ} {m' : Type uₘ} {n' : Type uₙ} {o' : Type uₒ} (A : Matrix m' n' α) (i : m') (row : Fin m → m') (col : o' → n') : A.submatrix (Matrix.vecCons i row) col = Matrix.vecCons (fun (j : o') => A i (col j)) (A.submatrix row col)

@[simp]

theorem Matrix.submatrix_updateRow_succAbove {α : Type u} {m : ℕ} {n' : Type uₙ} {o' : Type uₒ} (A : Matrix (Fin m.succ) n' α) (v : n' → α) (f : o' → n') (i : Fin m.succ) : (A.updateRow i v).submatrix i.succAbove f = A.submatrix i.succAbove f

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

@[simp]

theorem Matrix.submatrix_updateColumn_succAbove {α : Type u} {n : ℕ} {m' : Type uₘ} {o' : Type uₒ} (A : Matrix m' (Fin n.succ) α) (v : m' → α) (f : o' → m') (i : Fin n.succ) : (A.updateColumn i v).submatrix f i.succAbove = A.submatrix f i.succAbove

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

theorem Matrix.one_fin_two {α : Type u} [Zero α] [One α] : 1 = Matrix.of ![![1, 0], ![0, 1]]

theorem Matrix.one_fin_three {α : Type u} [Zero α] [One α] : 1 = Matrix.of ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]]

theorem Matrix.natCast_fin_two {α : Type u} [AddMonoidWithOne α] (n : ℕ) : ↑n = Matrix.of ![![↑n, 0], ![0, ↑n]]

theorem Matrix.natCast_fin_three {α : Type u} [AddMonoidWithOne α] (n : ℕ) : ↑n = Matrix.of ![![↑n, 0, 0], ![0, ↑n, 0], ![0, 0, ↑n]]

theorem Matrix.ofNat_fin_two {α : Type u} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] : OfNat.ofNat n = Matrix.of ![![OfNat.ofNat n, 0], ![0, OfNat.ofNat n]]

theorem Matrix.ofNat_fin_three {α : Type u} [AddMonoidWithOne α] (n : ℕ) [n.AtLeastTwo] : OfNat.ofNat n = Matrix.of ![![OfNat.ofNat n, 0, 0], ![0, OfNat.ofNat n, 0], ![0, 0, OfNat.ofNat n]]

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} [AddCommMonoid α] [Mul α] (a₁₁ : α) (a₁₂ : α) (a₂₁ : α) (a₂₂ : α) (b₁₁ : α) (b₁₂ : α) (b₂₁ : α) (b₂₂ : α) : Matrix.of ![![a₁₁, a₁₂], ![a₂₁, a₂₂]] * 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} [AddCommMonoid α] [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₃₃]] * 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} [Add α] (a₀ : α) (a₁ : α) (b₀ : α) (b₁ : α) : ![a₀, a₁] + ![b₀, b₁] = ![a₀ + b₀, a₁ + b₁]

theorem Matrix.vec3_add {α : Type u} [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} [SMul R α] (x : R) (a₀ : α) (a₁ : α) : x • ![a₀, a₁] = ![x • a₀, x • a₁]

theorem Matrix.smul_vec3 {α : Type u} {R : Type u_1} [SMul R α] (x : R) (a₀ : α) (a₁ : α) (a₂ : α) : x • ![a₀, a₁, a₂] = ![x • a₀, x • a₁, x • a₂]

theorem Matrix.vec2_dotProduct' {α : Type u} [AddCommMonoid α] [Mul α] {a₀ : α} {a₁ : α} {b₀ : α} {b₁ : α} : Matrix.dotProduct ![a₀, a₁] ![b₀, b₁] = a₀ * b₀ + a₁ * b₁

@[simp]

theorem Matrix.vec2_dotProduct {α : Type u} [AddCommMonoid α] [Mul α] (v : Fin 2 → α) (w : Fin 2 → α) : Matrix.dotProduct v w = v 0 * w 0 + v 1 * w 1

theorem Matrix.vec3_dotProduct' {α : Type u} [AddCommMonoid α] [Mul α] {a₀ : α} {a₁ : α} {a₂ : α} {b₀ : α} {b₁ : α} {b₂ : α} : Matrix.dotProduct ![a₀, a₁, a₂] ![b₀, b₁, b₂] = a₀ * b₀ + a₁ * b₁ + a₂ * b₂

@[simp]

theorem Matrix.vec3_dotProduct {α : Type u} [AddCommMonoid α] [Mul α] (v : Fin 3 → α) (w : Fin 3 → α) : Matrix.dotProduct v w = v 0 * w 0 + v 1 * w 1 + v 2 * w 2