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

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
        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 (Nat.succ m)) (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 (Nat.succ m)n'α) (j : n') :
        (Matrix.vecHead fun (i : Fin (Nat.succ m)) => B i j) = Matrix.vecHead B j
        @[simp]
        theorem Matrix.tail_val' {α : Type u} {m : } {n' : Type uₙ} (B : Fin (Nat.succ m)n'α) (j : n') :
        (Matrix.vecTail fun (i : Fin (Nat.succ m)) => 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 (Nat.succ n)α) :
        @[simp]
        theorem Matrix.dotProduct_cons {α : Type u} {n : } [AddCommMonoid α] [Mul α] (v : Fin (Nat.succ n)α) (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} (v : Fin 0α) :
        @[simp]
        theorem Matrix.col_cons {α : Type u} {m : } (x : α) (u : Fin mα) :
        @[simp]
        theorem Matrix.row_empty {α : Type u} :
        Matrix.row ![] = fun (x : Unit) => ![]
        @[simp]
        theorem Matrix.row_cons {α : Type u} {m : } (x : α) (u : Fin mα) :
        Matrix.row (Matrix.vecCons x u) = fun (x_1 : Unit) => Matrix.vecCons x u
        @[simp]
        theorem Matrix.transpose_empty_rows {α : Type u} {m' : Type uₘ} (A : Matrix m' (Fin 0) α) :
        Matrix.transpose A = Matrix.of ![]
        @[simp]
        theorem Matrix.transpose_empty_cols {α : Type u} {m' : Type uₘ} (A : Matrix (Fin 0) m' α) :
        Matrix.transpose A = Matrix.of fun (x : m') => ![]
        @[simp]
        theorem Matrix.cons_transpose {α : Type u} {m : } {n' : Type uₙ} (v : n'α) (A : Matrix (Fin m) n' α) :
        Matrix.transpose (Matrix.of (Matrix.vecCons v A)) = Matrix.of fun (i : n') => Matrix.vecCons (v i) (Matrix.transpose A i)
        @[simp]
        theorem Matrix.head_transpose {α : Type u} {n : } {m' : Type uₘ} (A : Matrix m' (Fin (Nat.succ n)) α) :
        Matrix.vecHead (Matrix.of.symm (Matrix.transpose A)) = Matrix.vecHead Matrix.of.symm A
        @[simp]
        theorem Matrix.tail_transpose {α : Type u} {n : } {m' : Type uₘ} (A : Matrix m' (Fin (Nat.succ n)) α) :
        Matrix.vecTail (Matrix.of.symm (Matrix.transpose A)) = 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 (Nat.succ m)) n' α) (B : Matrix n' o' α) (i : Fin m) (j : o') :
        (A * B) (Fin.succ i) 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 (Nat.succ n)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 (Nat.succ n)α) (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'α) :
        @[simp]
        theorem Matrix.mulVec_empty {α : Type u} {m' : Type uₘ} [NonUnitalNonAssocSemiring α] (A : Matrix m' (Fin 0) α) (v : Fin 0α) :
        @[simp]
        theorem Matrix.cons_mulVec {α : Type u} {m : } {n' : Type uₙ} [NonUnitalNonAssocSemiring α] [Fintype n'] (v : n'α) (A : Fin mn'α) (w : n'α) :
        Matrix.mulVec (Matrix.of (Matrix.vecCons v A)) w = Matrix.vecCons (Matrix.dotProduct v w) (Matrix.mulVec (Matrix.of A) w)
        @[simp]
        theorem Matrix.mulVec_cons {n : } {m' : Type uₘ} {α : Type u_1} [CommSemiring α] (A : m'Fin (Nat.succ n)α) (x : α) (v : Fin nα) :
        Matrix.mulVec (Matrix.of A) (Matrix.vecCons x v) = x Matrix.vecHead A + Matrix.mulVec (Matrix.of (Matrix.vecTail A)) 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 = 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) = 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') :
        Matrix.submatrix A 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') :
        Matrix.submatrix A (Matrix.vecCons i row) col = Matrix.vecCons (fun (j : o') => A i (col j)) (Matrix.submatrix A row col)
        @[simp]
        theorem Matrix.submatrix_updateRow_succAbove {α : Type u} {m : } {n' : Type uₙ} {o' : Type uₒ} (A : Matrix (Fin (Nat.succ m)) n' α) (v : n'α) (f : o'n') (i : Fin (Nat.succ m)) :

        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 (Nat.succ n)) α) (v : m'α) (f : o'm') (i : Fin (Nat.succ n)) :

        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 : ) [Nat.AtLeastTwo n] :
        OfNat.ofNat n = Matrix.of ![![OfNat.ofNat n, 0], ![0, OfNat.ofNat n]]
        theorem Matrix.ofNat_fin_three {α : Type u} [AddMonoidWithOne α] (n : ) [Nat.AtLeastTwo n] :
        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