Documentation

Mathlib.Data.Matrix.Notation

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]].

Examples #

Examples of usage can be found in the test/matrix.lean file.

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.
Instances For

    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.
    Instances For

      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.
      Instances For

        Delaborator for the !![] notation.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          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 mn'α) (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.succn'α) (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.succn'α) (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α) :
          @[simp]
          theorem Matrix.cons_dotProduct {α : Type u} {n : } [AddCommMonoid α] [Mul α] (x : α) (v : Fin nα) (w : Fin n.succα) :
          @[simp]
          theorem Matrix.dotProduct_cons {α : Type u} {n : } [AddCommMonoid α] [Mul α] (v : Fin n.succα) (x : α) (w : Fin nα) :
          theorem Matrix.cons_dotProduct_cons {α : Type u} {n : } [AddCommMonoid α] [Mul α] (x : α) (v : Fin nα) (y : α) (w : Fin nα) :
          @[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 mn'α) (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' α) :
          @[simp]
          theorem Matrix.vecMul_empty {α : Type u} {n' : Type uₙ} [NonUnitalNonAssocSemiring α] [Fintype n'] (v : n'α) (B : Matrix n' (Fin 0) α) :
          @[simp]
          theorem Matrix.cons_vecMul {α : Type u} {n : } {o' : Type uₒ} [NonUnitalNonAssocSemiring α] (x : α) (v : Fin nα) (B : Fin n.succo'α) :
          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 no'α) :
          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 no'α) :
          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 mn'α) (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'α) :
          @[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'α) :
          @[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 0m'α) :
          x A = ![]
          theorem Matrix.smul_mat_cons {α : Type u} {m : } {n' : Type uₙ} [NonUnitalNonAssocSemiring α] (x : α) (v : n'α) (A : Fin mn'α) :
          @[simp]
          theorem Matrix.submatrix_empty {α : Type u} {m' : Type uₘ} {n' : Type uₙ} {o' : Type uₒ} (A : Matrix m' n' α) (row : Fin 0m') (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 mm') (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 = !![1, 0; 0, 1]
          theorem Matrix.one_fin_three {α : Type u} [Zero α] [One α] :
          1 = !![1, 0, 0; 0, 1, 0; 0, 0, 1]
          theorem Matrix.natCast_fin_two {α : Type u} [AddMonoidWithOne α] (n : ) :
          n = !![n, 0; 0, n]
          theorem Matrix.natCast_fin_three {α : Type u} [AddMonoidWithOne α] (n : ) :
          n = !![n, 0, 0; 0, n, 0; 0, 0, n]
          theorem Matrix.ofNat_fin_two {α : Type u} [AddMonoidWithOne α] (n : ) [n.AtLeastTwo] :
          theorem Matrix.ofNat_fin_three {α : Type u} [AddMonoidWithOne α] (n : ) [n.AtLeastTwo] :
          OfNat.ofNat n = !![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 = !![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 = !![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₂₂ : α) :
          !![a₁₁, a₁₂; a₂₁, a₂₂] * !![b₁₁, b₁₂; b₂₁, b₂₂] = !![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₃₃ : α) :
          !![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.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