Matrix.submatrix_updateRow_succAbove
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
The theorem, `Matrix.submatrix_updateRow_succAbove`, states that for any type `α`, natural number `m`, types `n'` and `o'`, a matrix `A` with entries of type `α` and rows indexed by `Fin m.succ` and columns indexed by `n'`, a function `v` mapping `n'` to `α`, a function `f` mapping `o'` to `n'`, and an index `i` of type `Fin m.succ`, updating the row `i` of `A` with `v` and then removing the row just above `i` is equivalent to just removing the row just above `i` from `A` without any update. Here, `updateRow` is a function that updates a specified row of a matrix with a given function, `submatrix` is a function that removes a specified row from a matrix, and `i.succAbove` is a function that specifies the row just above `i`.
More concisely: For any matrix `A` with type `α` entries and indexed by `Fin (m + 1)`, updating row `(m)` with function `v` and removing row `(m - 1)` is equivalent to removing row `(m - 1)` without any update.
|
Matrix.cons_val'
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 => B i j) i
The theorem `Matrix.cons_val'` states that for any type `α`, natural number `m`, type `n'`, a function `v` mapping from `n'` to `α`, a function `B` mapping from `Fin m` to `n'` to `α`, and elements `i` of `Fin (Nat.succ m)` and `j` of `n'`, the operation of prepending the vector `v` to the matrix `B` and then selecting the `(i, j)`-th entry is the same as prepending the `j`-th entry of `v` to the `j`-th column of `B` and then selecting the `i`-th entry. In other words, constructing a matrix by appending a row and fetching a value from it is the same as appending an element to each column and fetching a value.
More concisely: For any type `α`, natural numbers `m` and `n`, functions `v : Fin n -> α` and `B : Fin m -> Fin n -> α`, elements `i : Fin (Nat.succ m)` and `j : Fin n`, the `(i, j)`-th entry of the matrix `[B : matrix α m n | v]` is equal to the `j`-th entry of the `j`-th column of the matrix `B` appended with the row `[v]`.
|
Matrix.vec3_add
theorem Matrix.vec3_add :
∀ {α : Type u} [inst : Add α] (a₀ a₁ a₂ b₀ b₁ b₂ : α),
![a₀, a₁, a₂] + ![b₀, b₁, b₂] = ![a₀ + b₀, a₁ + b₁, a₂ + b₂]
This theorem, `Matrix.vec3_add`, states that for any type `α` that supports an addition operation, given two 3-dimensional vectors (each represented as a list of three elements of type `α`), the addition of these two vectors results in a new vector where each corresponding pair of elements from the initial vectors is summed. This corresponds to the standard vector addition operation in mathematics, where vectors are added component-wise.
More concisely: For any type `α` with addition, the sum of two 3-vector columns of length 3 over `α` is a 3-vector column of length 3 over `α`, obtained by applying the component-wise addition of the corresponding entries.
|
Matrix.submatrix_updateColumn_succAbove
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
This theorem states that for any type `α`, natural number `n`, types `m'` and `o'`, given a matrix `A` with entries of type `α`, rows indexed by `m'` and columns indexed by `n + 1`, a function `v` from `m'` to `α` denoting a column update, a function `f` from `o'` to `m'`, and an index `i` within the range of `n + 1`, updating a column of the matrix and subsequently removing it is equivalent to just removing the column. In more mathematical terms, if we denote the operation of updating a column in `A` with `v` at index `i` as `(A.updateColumn i v)`, and denoting the operation of removing a column in a matrix at index `i.succAbove` as `.submatrix f i.succAbove`, the theorem states that these two operations commute, i.e., `(A.updateColumn i v).submatrix f i.succAbove = A.submatrix f i.succAbove`.
More concisely: For any matrix `A` with type `α` entries, indexed by `m'` rows and `n + 1` columns, function `v` from `m'` to `α` representing a column update, function `f` from `o'` to `m'`, and index `i` within the range of `n + 1`, updating column `i` with `v` and subsequently removing it is equivalent to removing column `i` directly: `(A.updateColumn i v).submatrix f i.succAbove = A.submatrix f i.succAbove`.
|
Matrix.dotProduct_cons
theorem Matrix.dotProduct_cons :
∀ {α : Type u} {n : ℕ} [inst : AddCommMonoid α] [inst_1 : 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
The theorem `Matrix.dotProduct_cons` states that for any type `α` with addition and multiplication structures, for any natural number `n`, and any vectors `v` of length `n+1` and `w` of length `n`, and any element `x` of type `α`, the dot product of `v` with a vector obtained by prepending `x` to `w` is equal to the product of the first element of `v` and `x`, plus the dot product of the remaining elements of `v` (after removing the first element) and `w`. In terms of mathematical notation, if `v = (v1, v2, ..., vn+1)` and `w = (w1, w2, ..., wn)`, then `v . (x, w) = v1*x + (v2, ..., vn+1) . w`.
More concisely: For any type `α` with addition and multiplication structures, and vectors `v` of length `n+1` and `w` of length `n` over `α`, the dot product of `v` with the vector `(x :: w)` is equal to `v.1 * x + ⟨v.2, ..., v.n+1⟩ . w`.
|
Matrix.vec3_eq
theorem Matrix.vec3_eq :
∀ {α : Type u} {a₀ a₁ a₂ b₀ b₁ b₂ : α}, a₀ = b₀ → a₁ = b₁ → a₂ = b₂ → ![a₀, a₁, a₂] = ![b₀, b₁, b₂]
This theorem states that for any type `α`, given pairs of elements `a₀, a₁, a₂` and `b₀, b₁, b₂` of type `α`, if `a₀` equals `b₀`, `a₁` equals `b₁`, and `a₂` equals `b₂`, then the vector formed from `a₀, a₁, a₂` is equal to the vector formed from `b₀, b₁, b₂`. Each pair of elements forms the corresponding entries of the two vectors, so this theorem essentially ensures that two vectors are equal if and only if their corresponding entries are equal.
More concisely: For any type `α`, if `(a₀, a₁, a₂) = (b₀, b₁, b₂)` are equal tuples of elements of type `α`, then the vectors `[a₀, a₁, a₂]` and `[b₀, b₁, b₂]` are equal.
|