Documentation

Mathlib.Data.Matrix.RowCol

Row and column matrices #

This file provides results about row and column matrices

Main definitions #

source
def Matrix.col {m : Type u_2} {α : Type v} (w : m → α) :
Matrix m Unit α

Matrix.col u is the column matrix whose entries are given by u.

Equations
Instances For
    source
    @[simp]
    theorem Matrix.col_apply {m : Type u_2} {α : Type v} (w : m → α) (i : m) (j : Unit) :
    Matrix.col w i j = w i
    source
    def Matrix.row {n : Type u_3} {α : Type v} (v : n → α) :
    Matrix Unit n α

    Matrix.row u is the row matrix whose entries are given by u.

    Equations
    Instances For
      source
      @[simp]
      theorem Matrix.row_apply {n : Type u_3} {α : Type v} (v : n → α) (i : Unit) (j : n) :
      Matrix.row v i j = v j
      source
      theorem Matrix.col_injective {m : Type u_2} {α : Type v} :
      Function.Injective Matrix.col
      source
      @[simp]
      theorem Matrix.col_inj {m : Type u_2} {α : Type v} {v : m → α} {w : m → α} :
      Matrix.col v = Matrix.col w ↔ v = w
      source
      @[simp]
      theorem Matrix.col_zero {m : Type u_2} {α : Type v} [Zero α] :
      Matrix.col 0 = 0
      source
      @[simp]
      theorem Matrix.col_eq_zero {m : Type u_2} {α : Type v} [Zero α] (v : m → α) :
      Matrix.col v = 0 ↔ v = 0
      source
      @[simp]
      theorem Matrix.col_add {m : Type u_2} {α : Type v} [Add α] (v : m → α) (w : m → α) :
      Matrix.col (v + w) = Matrix.col v + Matrix.col w
      source
      @[simp]
      theorem Matrix.col_smul {m : Type u_2} {R : Type u_5} {α : Type v} [SMul R α] (x : R) (v : m → α) :
      Matrix.col (x • v) = x • Matrix.col v
      source
      theorem Matrix.row_injective {n : Type u_3} {α : Type v} :
      Function.Injective Matrix.row
      source
      @[simp]
      theorem Matrix.row_inj {n : Type u_3} {α : Type v} {v : n → α} {w : n → α} :
      Matrix.row v = Matrix.row w ↔ v = w
      source
      @[simp]
      theorem Matrix.row_zero {n : Type u_3} {α : Type v} [Zero α] :
      Matrix.row 0 = 0
      source
      @[simp]
      theorem Matrix.row_eq_zero {n : Type u_3} {α : Type v} [Zero α] (v : n → α) :
      Matrix.row v = 0 ↔ v = 0
      source
      @[simp]
      theorem Matrix.row_add {m : Type u_2} {α : Type v} [Add α] (v : m → α) (w : m → α) :
      Matrix.row (v + w) = Matrix.row v + Matrix.row w
      source
      @[simp]
      theorem Matrix.row_smul {m : Type u_2} {R : Type u_5} {α : Type v} [SMul R α] (x : R) (v : m → α) :
      Matrix.row (x • v) = x • Matrix.row v
      source
      @[simp]
      theorem Matrix.transpose_col {m : Type u_2} {α : Type v} (v : m → α) :
      Matrix.transpose (Matrix.col v) = Matrix.row v
      source
      @[simp]
      theorem Matrix.transpose_row {m : Type u_2} {α : Type v} (v : m → α) :
      Matrix.transpose (Matrix.row v) = Matrix.col v
      source
      @[simp]
      theorem Matrix.conjTranspose_col {m : Type u_2} {α : Type v} [Star α] (v : m → α) :
      Matrix.conjTranspose (Matrix.col v) = Matrix.row (star v)
      source
      @[simp]
      theorem Matrix.conjTranspose_row {m : Type u_2} {α : Type v} [Star α] (v : m → α) :
      Matrix.conjTranspose (Matrix.row v) = Matrix.col (star v)
      source
      theorem Matrix.row_vecMul {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : m → α) :
      Matrix.row (Matrix.vecMul v M) = Matrix.row v * M
      source
      theorem Matrix.col_vecMul {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : m → α) :
      Matrix.col (Matrix.vecMul v M) = Matrix.transpose (Matrix.row v * M)
      source
      theorem Matrix.col_mulVec {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype n] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : n → α) :
      Matrix.col (Matrix.mulVec M v) = M * Matrix.col v
      source
      theorem Matrix.row_mulVec {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype n] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : n → α) :
      Matrix.row (Matrix.mulVec M v) = Matrix.transpose (M * Matrix.col v)
      source
      @[simp]
      theorem Matrix.row_mul_col_apply {m : Type u_2} {α : Type v} [Fintype m] [Mul α] [AddCommMonoid α] (v : m → α) (w : m → α) (i : Unit) (j : Unit) :
      (Matrix.row v * Matrix.col w) i j = Matrix.dotProduct v w
      source
      @[simp]
      theorem Matrix.diag_col_mul_row {n : Type u_3} {α : Type v} [Mul α] [AddCommMonoid α] (a : n → α) (b : n → α) :
      Matrix.diag (Matrix.col a * Matrix.row b) = a * b
      source
      theorem Matrix.vecMulVec_eq {m : Type u_2} {n : Type u_3} {α : Type v} [Mul α] [AddCommMonoid α] (w : m → α) (v : n → α) :
      Matrix.vecMulVec w v = Matrix.col w * Matrix.row v

      Updating rows and columns #

      source
      def Matrix.updateRow {m : Type u_2} {n : Type u_3} {α : Type v} [DecidableEq m] (M : Matrix m n α) (i : m) (b : n → α) :
      Matrix m n α

      Update, i.e. replace the ith row of matrix A with the values in b.

      Equations
      Instances For
        source
        def Matrix.updateColumn {m : Type u_2} {n : Type u_3} {α : Type v} [DecidableEq n] (M : Matrix m n α) (j : n) (b : m → α) :
        Matrix m n α

        Update, i.e. replace the jth column of matrix A with the values in b.

        Equations
        Instances For
          source
          @[simp]
          theorem Matrix.updateRow_self {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {b : n → α} [DecidableEq m] :
          Matrix.updateRow M i b i = b
          source
          @[simp]
          theorem Matrix.updateColumn_self {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {j : n} {c : m → α} [DecidableEq n] :
          Matrix.updateColumn M j c i j = c i
          source
          @[simp]
          theorem Matrix.updateRow_ne {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {b : n → α} [DecidableEq m] {i' : m} (i_ne : i' ≠ i) :
          Matrix.updateRow M i b i' = M i'
          source
          @[simp]
          theorem Matrix.updateColumn_ne {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {j : n} {c : m → α} [DecidableEq n] {j' : n} (j_ne : j' ≠ j) :
          Matrix.updateColumn M j c i j' = M i j'
          source
          theorem Matrix.updateRow_apply {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {j : n} {b : n → α} [DecidableEq m] {i' : m} :
          Matrix.updateRow M i b i' j = if i' = i then b j else M i' j
          source
          theorem Matrix.updateColumn_apply {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {j : n} {c : m → α} [DecidableEq n] {j' : n} :
          Matrix.updateColumn M j c i j' = if j' = j then c i else M i j'
          source
          @[simp]
          theorem Matrix.updateColumn_subsingleton {m : Type u_2} {n : Type u_3} {R : Type u_5} [Subsingleton n] (A : Matrix m n R) (i : n) (b : m → R) :
          Matrix.updateColumn A i b = Matrix.submatrix (Matrix.col b) id (Function.const n ())
          source
          @[simp]
          theorem Matrix.updateRow_subsingleton {m : Type u_2} {n : Type u_3} {R : Type u_5} [Subsingleton m] (A : Matrix m n R) (i : m) (b : n → R) :
          Matrix.updateRow A i b = Matrix.submatrix (Matrix.row b) (Function.const m ()) id
          source
          theorem Matrix.map_updateRow {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {M : Matrix m n α} {i : m} {b : n → α} [DecidableEq m] (f : α → β) :
          Matrix.map (Matrix.updateRow M i b) f = Matrix.updateRow (Matrix.map M f) i (f ∘ b)
          source
          theorem Matrix.map_updateColumn {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {M : Matrix m n α} {j : n} {c : m → α} [DecidableEq n] (f : α → β) :
          Matrix.map (Matrix.updateColumn M j c) f = Matrix.updateColumn (Matrix.map M f) j (f ∘ c)
          source
          theorem Matrix.updateRow_transpose {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {j : n} {c : m → α} [DecidableEq n] :
          Matrix.updateRow (Matrix.transpose M) j c = Matrix.transpose (Matrix.updateColumn M j c)
          source
          theorem Matrix.updateColumn_transpose {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {b : n → α} [DecidableEq m] :
          Matrix.updateColumn (Matrix.transpose M) i b = Matrix.transpose (Matrix.updateRow M i b)
          source
          theorem Matrix.updateRow_conjTranspose {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {j : n} {c : m → α} [DecidableEq n] [Star α] :
          Matrix.updateRow (Matrix.conjTranspose M) j (star c) = Matrix.conjTranspose (Matrix.updateColumn M j c)
          source
          theorem Matrix.updateColumn_conjTranspose {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {b : n → α} [DecidableEq m] [Star α] :
          Matrix.updateColumn (Matrix.conjTranspose M) i (star b) = Matrix.conjTranspose (Matrix.updateRow M i b)
          source
          @[simp]
          theorem Matrix.updateRow_eq_self {m : Type u_2} {n : Type u_3} {α : Type v} [DecidableEq m] (A : Matrix m n α) (i : m) :
          Matrix.updateRow A i (A i) = A
          source
          @[simp]
          theorem Matrix.updateColumn_eq_self {m : Type u_2} {n : Type u_3} {α : Type v} [DecidableEq n] (A : Matrix m n α) (i : n) :
          (Matrix.updateColumn A i fun (j : m) => A j i) = A
          source
          theorem Matrix.diagonal_updateColumn_single {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] (v : n → α) (i : n) (x : α) :
          Matrix.updateColumn (Matrix.diagonal v) i (Pi.single i x) = Matrix.diagonal (Function.update v i x)
          source
          theorem Matrix.diagonal_updateRow_single {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] (v : n → α) (i : n) (x : α) :
          Matrix.updateRow (Matrix.diagonal v) i (Pi.single i x) = Matrix.diagonal (Function.update v i x)

          Updating rows and columns commutes in the obvious way with reindexing the matrix.

          source
          theorem Matrix.updateRow_submatrix_equiv {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [DecidableEq l] [DecidableEq m] (A : Matrix m n α) (i : l) (r : o → α) (e : l ≃ m) (f : o ≃ n) :
          Matrix.updateRow (Matrix.submatrix A ⇑e ⇑f) i r = Matrix.submatrix (Matrix.updateRow A (e i) fun (j : n) => r (f.symm j)) ⇑e ⇑f
          source
          theorem Matrix.submatrix_updateRow_equiv {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [DecidableEq l] [DecidableEq m] (A : Matrix m n α) (i : m) (r : n → α) (e : l ≃ m) (f : o ≃ n) :
          Matrix.submatrix (Matrix.updateRow A i r) ⇑e ⇑f = Matrix.updateRow (Matrix.submatrix A ⇑e ⇑f) (e.symm i) fun (i : o) => r (f i)
          source
          theorem Matrix.updateColumn_submatrix_equiv {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [DecidableEq o] [DecidableEq n] (A : Matrix m n α) (j : o) (c : l → α) (e : l ≃ m) (f : o ≃ n) :
          Matrix.updateColumn (Matrix.submatrix A ⇑e ⇑f) j c = Matrix.submatrix (Matrix.updateColumn A (f j) fun (i : m) => c (e.symm i)) ⇑e ⇑f
          source
          theorem Matrix.submatrix_updateColumn_equiv {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [DecidableEq o] [DecidableEq n] (A : Matrix m n α) (j : n) (c : m → α) (e : l ≃ m) (f : o ≃ n) :
          Matrix.submatrix (Matrix.updateColumn A j c) ⇑e ⇑f = Matrix.updateColumn (Matrix.submatrix A ⇑e ⇑f) (f.symm j) fun (i : l) => c (e i)

          reindex versions of the above submatrix lemmas for convenience.

          source
          theorem Matrix.updateRow_reindex {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [DecidableEq l] [DecidableEq m] (A : Matrix m n α) (i : l) (r : o → α) (e : m ≃ l) (f : n ≃ o) :
          Matrix.updateRow ((Matrix.reindex e f) A) i r = (Matrix.reindex e f) (Matrix.updateRow A (e.symm i) fun (j : n) => r (f j))
          source
          theorem Matrix.reindex_updateRow {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [DecidableEq l] [DecidableEq m] (A : Matrix m n α) (i : m) (r : n → α) (e : m ≃ l) (f : n ≃ o) :
          (Matrix.reindex e f) (Matrix.updateRow A i r) = Matrix.updateRow ((Matrix.reindex e f) A) (e i) fun (i : o) => r (f.symm i)
          source
          theorem Matrix.updateColumn_reindex {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [DecidableEq o] [DecidableEq n] (A : Matrix m n α) (j : o) (c : l → α) (e : m ≃ l) (f : n ≃ o) :
          Matrix.updateColumn ((Matrix.reindex e f) A) j c = (Matrix.reindex e f) (Matrix.updateColumn A (f.symm j) fun (i : m) => c (e i))
          source
          theorem Matrix.reindex_updateColumn {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [DecidableEq o] [DecidableEq n] (A : Matrix m n α) (j : n) (c : m → α) (e : m ≃ l) (f : n ≃ o) :
          (Matrix.reindex e f) (Matrix.updateColumn A j c) = Matrix.updateColumn ((Matrix.reindex e f) A) (f j) fun (i : l) => c (e.symm i)