Matrix.smul_cons
theorem Matrix.smul_cons :
∀ {α : Type u} {n : ℕ} {M : Type u_4} [inst : SMul M α] (x : M) (y : α) (v : Fin n → α),
x • Matrix.vecCons y v = Matrix.vecCons (x • y) (x • v)
This theorem states that for any scalar multiplication operation (`SMul`), given a scalar `x` of type `M`, an element `y` of type `α`, and a vector function `v` (a function from the finite set of size `n` to `α`), the scalar multiplication of `x` with the vector formed by prepending `y` to `v` (`Matrix.vecCons y v`) is equivalent to the vector obtained by prepending `x` multiplied by `y` to `x` multiplied by `v`. In other words, scalar multiplication distributes over the vector concatenation operation, `vecCons`.
More concisely: For any scalar `x` and vector `v` of length `n+1`, and any element `y`, the scalar multiplication of `x` with the vector obtained by prepending `y` to `v` (`Matrix.vecCons y v`) is equal to the vector obtained by prepending the product of `x` and `y` to the result of multiplying `x` with `v`. In other words, `x * (Matrix.vecCons y v) = Matrix.vecCons (x * y) (x * v)`.
|
Matrix.cons_val_succ
theorem Matrix.cons_val_succ :
∀ {α : Type u} {m : ℕ} (x : α) (u : Fin m → α) (i : Fin m), Matrix.vecCons x u i.succ = u i
The theorem `Matrix.cons_val_succ` is stating that for any type `α`, any natural number `m`, any value `x` of type `α`, any function `u` from `Fin m` to `α`, and any value `i` in `Fin m`, if you prepend the value `x` to the vector defined by function `u` using `Matrix.vecCons` and then access the element at the position `Fin.succ i` (which is the successor of `i`), it will be equal to the the element at position `i` in the original vector defined by `u`. This essentially says that indices in the new vector with `Matrix.vecCons` are shifted by one compared to the original vector.
More concisely: For any type `α`, any natural number `m`, any function `u` from `Fin m` to `α`, and any indices `i`, `Matrix.vecCons (x :: u) i = u i.prev`, where `prev` denotes the predecessor of `i`.
|
Matrix.tail_cons
theorem Matrix.tail_cons : ∀ {α : Type u} {m : ℕ} (x : α) (u : Fin m → α), Matrix.vecTail (Matrix.vecCons x u) = u := by
sorry
The theorem `Matrix.tail_cons` states that for any type `α`, any natural number `m`, any element `x` of type `α`, and any vector `u` of size `m` with elements of type `α`, if we prepend `x` to `u` using `Matrix.vecCons` and then remove the first element of the resulting vector using `Matrix.vecTail`, we get back the original vector `u`. This essentially proves the property that `Matrix.vecTail` and `Matrix.vecCons` are inverse of each other in the sense that prepending an element on a vector and then removing the first element of the resulting vector gives back the original vector.
More concisely: For any type `α` and natural number `m`, the operations `Matrix.vecCons` and `Matrix.vecTail` on vectors of size `m+1` satisfy `Matrix.vecTail (Matrix.vecCons x u) = u`, where `x` is an element of type `α` and `u` is a vector of size `m` with elements of type `α`.
|
Matrix.smul_empty
theorem Matrix.smul_empty : ∀ {α : Type u} {M : Type u_4} [inst : SMul M α] (x : M) (v : Fin 0 → α), x • v = ![] := by
sorry
This theorem, named `Matrix.smul_empty`, states that for any type `α` and type `M`, given an instance of scalar multiplication (`SMul`) for `M` and `α`, for any scalar `x` of type `M` and any vector `v` of size 0 (an empty vector), the scalar multiplication of `x` and `v` is an empty vector. In other words, if you multiply a scalar with an empty vector, the result is an empty vector.
More concisely: For any type `α` and matrix `M`, if `M` has scalar multiplication with scalar `α`, then the scalar multiplication of any scalar `x` in `M` with the empty vector of size `1` in `M` is the empty vector.
|
Matrix.empty_val'
theorem Matrix.empty_val' : ∀ {α : Type u} {n' : Type u_4} (j : n'), (fun i => ![]) = ![]
This theorem states that for any given type `α` and `n'`, and for any value `j` of type `n'`, the function which maps any index `i` to an empty list is itself an empty list. Essentially, it's saying that an empty matrix (represented as a function from indices to lists) is equivalent to an empty list, no matter what type the indices or elements of the matrix are.
More concisely: For any type `α` and natural number `n`, the function from indices `i` to empty lists `[] : List α` is equal to the empty list `[] : List (List α)`.
|
Matrix.range_empty
theorem Matrix.range_empty : ∀ {α : Type u} (u : Fin 0 → α), Set.range u = ∅
This theorem states that for any function `u` from an empty finite set (of type `Fin 0`) to any type `α`, the range of the function `u` is the empty set. In other words, there are no elements in the codomain `α` that `u` can map to from an empty domain. This is expressed mathematically as: for all functions `u` from `Fin 0` to `α`, the range of `u` equals the empty set.
More concisely: For any function from a finite empty set to any type, its range is the empty set.
|
Matrix.range_cons
theorem Matrix.range_cons :
∀ {α : Type u} {n : ℕ} (x : α) (u : Fin n → α), Set.range (Matrix.vecCons x u) = {x} ∪ Set.range u
This theorem states that for any type `α` and any natural number `n`, given any element `x` of the type `α` and a function `u` from the finite set of size `n` to `α`, the range of the function that prepends `x` to the vector formed by `u` is the set containing `x` union the range of `u`. In other words, it's saying that if you prepend the element `x` to a vector, the set of possible values the vector can take includes `x` and all the values the original vector could take.
More concisely: For any type `α` and natural number `n`, if `x` is an element of `α` and `u` is a function from a finite set of size `n` to `α`, then the range of the function `x :: u` (the function that prepends `x` to `u`'s range) equals `{x} ∪ u(`range(u)`)`.
|
Matrix.vecAppend_eq_ite
theorem Matrix.vecAppend_eq_ite :
∀ {m n : ℕ} {α : Type u_4} {o : ℕ} (ho : o = m + n) (u : Fin m → α) (v : Fin n → α),
Matrix.vecAppend ho u v = fun i => if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩
This theorem `Matrix.vecAppend_eq_ite` states that for any natural numbers `m` and `n`, and for any type `α`, given a specific natural number `o` that equals `m + n`, and two functions `u` and `v` that map from `Fin m` and `Fin n` to `α` respectively, the `Matrix.vecAppend` function applied to `ho`, `u` and `v` results in a function that maps from `Fin o` to `α`. This resultant function behaves as follows: for any input `i`, if the coerced value of `i` is less than `m`, it returns the output of `u` for `i` (adjusted with respect to `m`); otherwise, it returns the output of `v` for `i` (adjusted with respect to `m`). Here, `Fin n` is a finite set of natural numbers less than `n`.
More concisely: For any natural numbers m and n, and type α, the function `Matrix.vecAppend u v` on inputs from `Fin (m + n)` is equal to the function defined by `ite (< m) u (m + _ => v)`, where `u` is a function from `Fin m` to α and `v` is a function from `Fin n` to α.
|
Matrix.cons_val_one
theorem Matrix.cons_val_one :
∀ {α : Type u} {m : ℕ} (x : α) (u : Fin m.succ → α), Matrix.vecCons x u 1 = Matrix.vecHead u
The theorem `Matrix.cons_val_one` states that for any type `α`, natural number `m`, an element `x` of type `α`, and a function `u` from `Fin m.succ` to `α`, the second element (indexed by `1`) of a vector that was constructed by prepending `x` to the vector determined by `u` is the same as the first element of the vector determined by `u`. This theorem is needed for simplifying expressions when the length of the vector is `≥ 2`, due to an identity between `1` and `0` in the finite set `Fin 1`.
More concisely: For any type `α`, natural number `m`, element `x` of type `α`, and function `u` from `Fin (m+1)` to `α`, the first and second elements of the vector obtained by appending `x` to the vector determined by `u` are equal.
|
Matrix.cons_fin_one
theorem Matrix.cons_fin_one : ∀ {α : Type u} (x : α) (u : Fin 0 → α), Matrix.vecCons x u = fun x_1 => x
The theorem `Matrix.cons_fin_one` states that for all types `α`, given an element `x` of type `α` and a function `u` from `Fin 0` to `α`, applying the function `Matrix.vecCons` to `x` and `u` results in a function that maps any input to `x`. In other words, this theorem states that when you create a vector by prepending `x` to a vector of zero length (which is represented by the function `u`), you obtain a vector where every element is `x`.
More concisely: For any type `α` and element `x` of `α`, the function obtained by prepending `x` to the empty vector using `Matrix.vecCons` is the constant function mapping every index to `x`.
|
Matrix.cons_add_cons
theorem Matrix.cons_add_cons :
∀ {α : Type u} {n : ℕ} [inst : Add α] (x : α) (v : Fin n → α) (y : α) (w : Fin n → α),
Matrix.vecCons x v + Matrix.vecCons y w = Matrix.vecCons (x + y) (v + w)
The theorem `Matrix.cons_add_cons` states that for any type `α` that has an addition operation, any natural number `n`, and any two elements `x` and `y` of type `α`, as well as any two vectors `v` and `w` of length `n` with elements of type `α`, the sum of two vectors constructed by prepending `x` and `y` to `v` and `w`, respectively, is a new vector constructed by prepending the sum of `x` and `y` to the sum of `v` and `w`. In essence, it states that the operation of constructing a vector by prepending an element commutes with vector addition.
More concisely: For any type `α` with addition, and vectors `v`, `w` of length `n` over `α`, the operation of prepending an element to a vector commutes with vector addition: `[x] ++ (v ++ w) = ([x] ++ v) ++ w`, where `[x]` is the vector prepended with `x`.
|
Matrix.cons_val_fin_one
theorem Matrix.cons_val_fin_one : ∀ {α : Type u} (x : α) (u : Fin 0 → α) (i : Fin 1), Matrix.vecCons x u i = x := by
sorry
This theorem asserts that for any type `α`, any element `x` of type `α`, any function `u` from `Fin 0` to `α`, and any element `i` from `Fin 1`, applying the `Matrix.vecCons` function to `x`, `u`, and `i` always results in `x`. In other words, when a single-element vector is constructed by prepending `x` to a zero-element vector, the resulting vector's only element is `x` regardless of the index `i`.
More concisely: For any type `α`, any element `x` of type `α`, and any function `u : Fin 0 → α`, the application of `Matrix.vecCons x u 0` is equal to `x`.
|
Matrix.empty_add_empty
theorem Matrix.empty_add_empty : ∀ {α : Type u} [inst : Add α] (v w : Fin 0 → α), v + w = ![]
This theorem states that for any type `α` that supports addition, the sum of two empty vectors, `v` and `w`, of type `α` is an empty vector. In other words, if we take two vectors of size 0 (thus empty) and add them together, the result is another empty vector. This theorem follows logically from the fact that the sum of two empty structures is always empty, valid under the assumption that the type `α` allows for an addition operation.
More concisely: For any type `α` with an addition operation, the sum of two empty vectors of type `α` is an empty vector.
|
Matrix.zero_empty
theorem Matrix.zero_empty : ∀ {α : Type u} [inst : Zero α], 0 = ![]
This theorem states that for any type `α` that has a zero element (as specified by the `Zero α` typeclass), the zero matrix is represented as an empty list. Essentially, it denotes that an empty matrix is equivalent to the zero matrix in the context of a type that supports a zero element.
More concisely: For any type `α` with a zero element, the zero matrix is represented as an empty list. Equivalently, an empty matrix is the matrix representation of the additive identity for type `α`.
|
Matrix.empty_eq
theorem Matrix.empty_eq : ∀ {α : Type u} (v : Fin 0 → α), v = ![]
This theorem states that for any type `α` and any function `v` that maps from the finite type of size 0 (essentially an empty set) to `α`, `v` is equal to an empty list. In other words, any function from an empty set to some type can only be represented as an empty list in the context of matrices.
More concisely: For any type `α` and any function `v : Fin 0 → α`, `v` is equal to the empty list `[] : list α`.
|