Matrix.updateColumn_self
theorem Matrix.updateColumn_self :
∀ {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {j : n} {c : m → α} [inst : DecidableEq n],
M.updateColumn j c i j = c i
The theorem `Matrix.updateColumn_self` asserts that for any type `m` indexing the rows, type `n` indexing the columns, and type `α` representing the entries of a matrix `M`, along with a specific row `i`, column `j`, and column vector `c` (which is a function from `m` to `α`), if the equality of type `n` (the type indexing the columns) is decidable, then the `j`th column of the matrix `M` updated with the column vector `c` at row `i` and column `j` equals the `i`th element of the column vector `c`. In other words, when you replace the `j`th column of a matrix with a new column, the entry in the `i`th row and `j`th column of the updated matrix will be the `i`th element of the new column.
More concisely: If `M` is a matrix with decidable column equality, then updating the `j`th column of `M` with the column vector `c` results in a matrix where the entry in the `i`th row and `j`th column equals the `i`th element of `c`.
|
Matrix.updateColumn_ne
theorem Matrix.updateColumn_ne :
∀ {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {j : n} {c : m → α} [inst : DecidableEq n]
{j' : n}, j' ≠ j → M.updateColumn j c i j' = M i j'
The theorem `Matrix.updateColumn_ne` states that, for any given matrix `M` with entries of type `α`, indexed by types `m` and `n` for rows and columns respectively, and for any `i` of type `m`, `j` and `j'` of type `n`, and a function `c` from `m` to `α`. If we update the `j`th column of `M` with the values given by function `c`, and we have `j` not equal to `j'`, then the entry in the `i`th row and `j'`th column of the updated matrix is the same as the entry in the `i`th row and `j'`th column of the original matrix `M`. This theorem relies on the ability to decide equality between elements of type `n`.
More concisely: For any matrix M with entries of type α indexed by m and n, and any i of type m, j, j' of type n, and function c from m to α, if we update the j-th column of M with values given by c and j ≠ j', then the (i, j')-th entry of the updated matrix is equal to the (i, j')-th entry of the original matrix M.
|
Matrix.updateRow_transpose
theorem Matrix.updateRow_transpose :
∀ {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {j : n} {c : m → α} [inst : DecidableEq n],
M.transpose.updateRow j c = (M.updateColumn j c).transpose
The theorem `Matrix.updateRow_transpose` states that for any matrix `M` with entries of type `α`, row indices of type `m`, column indices of type `n`, any column index `j` and any function `c` from `m` to `α`, updating the `j`-th row of the transpose of `M` with the values given by `c` is the same as taking the transpose of the matrix formed by updating the `j`-th column of `M` with the values given by `c`. This is under the assumption that the equality of elements of type `n` is decidable.
More concisely: For any matrix M with decidably equal column indices and entries of type α, updating the j-th row of its transpose with values given by a function c is equivalent to taking the transpose of the matrix obtained by updating the j-th column of M with values given by c.
|
Matrix.updateRow_self
theorem Matrix.updateRow_self :
∀ {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {b : n → α} [inst : DecidableEq m],
M.updateRow i b i = b
The theorem `Matrix.updateRow_self` states that for any given matrix `M` with entries of type `α`, indexed by `m` for rows and `n` for columns, and for any function `b` mapping indices `n` to entries `α`, if we update the `i`th row of matrix `M` with the values given by `b`, then when we access the `i`th row of the updated matrix, we get the exact function `b` back. This is under the condition that equality is decidable for the row indices `m`. In other words, replacing the `i`th row of a matrix with a certain function results in that function when we look at the `i`th row of the resulting matrix.
More concisely: For any matrix `M` of type `α` with decidable row equality, updating the `i`th row with function `b` results in a matrix where the `i`th row equals `b`.
|
Matrix.updateRow_apply
theorem Matrix.updateRow_apply :
∀ {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {j : n} {b : n → α} [inst : DecidableEq m]
{i' : m}, M.updateRow i b i' j = if i' = i then b j else M i' j
This theorem states that for any type `m` indexing rows, type `n` indexing columns, and type `α` for entry values of a matrix `M`, along with a specific row `i` in `m`, a specific column `j` in `n`, and a function `b` mapping `n` to `α`, and given that equality in `m` is decidable, then updating the `i`-th row of the matrix `M` using function `b` and checking the value at the position `(i', j)` in the updated matrix results in the value `b j` if `i'` equals `i`, otherwise it remains the original value `M i' j`. This theorem precisely describes how a row in a matrix is updated with a new function in Lean 4.
More concisely: Given a decidably equated matrix M with types m for rows, n for columns, and α for entries, and a function b from n to α, updating row i of M with b results in the value b j for position (i, j), and the original value otherwise.
|
Matrix.updateRow_submatrix_equiv
theorem Matrix.updateRow_submatrix_equiv :
∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : DecidableEq l]
[inst_1 : DecidableEq m] (A : Matrix m n α) (i : l) (r : o → α) (e : l ≃ m) (f : o ≃ n),
(A.submatrix ⇑e ⇑f).updateRow i r = (A.updateRow (e i) fun j => r (f.symm j)).submatrix ⇑e ⇑f
This theorem states that for any types `l`, `m`, `n`, `o`, and `α` where `l` and `m` have decidable equality, given a matrix `A` indexed by `m` and `n` with entries in `α`, an index `i` of type `l`, a function `r` mapping `o` to `α`, and bijections `e` from `l` to `m` and `f` from `o` to `n`, updating the `i`th row of the submatrix of `A` obtained by applying `e` and `f` (via `Matrix.submatrix`) is equivalent to first updating the `(e i)`th row of `A` with `r` composed with the inverse of `f`, and then forming the submatrix with `e` and `f`.
More concisely: For matrices A indexed by types m and n with decidable equality, updating the i-th row of the submatrix obtained by bijections e from l to m and f from o to n is equivalent to first updating the (ei)-th row with r composed with the inverse of f, and then forming the submatrix with e and f.
|
Matrix.updateColumn_transpose
theorem Matrix.updateColumn_transpose :
∀ {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {b : n → α} [inst : DecidableEq m],
M.transpose.updateColumn i b = (M.updateRow i b).transpose
The theorem `Matrix.updateColumn_transpose` states that for any type `m` and `n` indicating the rows and columns of a matrix respectively, and any type `α` representing the content of the matrix, given a matrix `M` of type `Matrix m n α`, an index `i` of type `m` and a function `b` mapping from type `n` to type `α`, if equality of type `m` is decidable, then updating the `i`th column of the transpose of `M` with the values in `b` is equivalent to transposing the result of updating the `i`th row of `M` with the values in `b`. In other words, transposing a matrix after updating one of its columns has the same effect as first updating the corresponding row of the original matrix and then transposing it.
More concisely: For any matrix `M` of type `m x n α`, index `i`, and function `b`, if `m` has decidable equality, then updating the `i`th column of the transpose of `M` with `b` is equivalent to transposing the matrix obtained by updating the `i`th row of `M` with `b`.
|
Matrix.updateColumn_apply
theorem Matrix.updateColumn_apply :
∀ {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {j : n} {c : m → α} [inst : DecidableEq n]
{j' : n}, M.updateColumn j c i j' = if j' = j then c i else M i j'
The theorem `Matrix.updateColumn_apply` states that for any types `m` and `n`, any type `α` which has decidable equality, any matrix `M` with entries in `α` and indexed by `m` and `n`, any elements `i` of type `m` and `j` and `j'` of type `n`, and any function `c` from `m` to `α`, the entry at position `(i, j')` of the matrix obtained by updating the column `j` of `M` with the values provided by `c` is `c i` if `j'` is equal to `j`, and is the original entry `M i j'` otherwise. This theorem provides a precise specification for the behavior of the `Matrix.updateColumn` function.
More concisely: For any matrix `M` with decidable equality entries, updating column `j` of `M` with values `c(i)` results in a matrix where the entry at position `(i, j')` is `c(i)` if `j' = j` and the original entry `M(i, j')` otherwise.
|