Matrix.circulant_smul
theorem Matrix.circulant_smul :
∀ {α : Type u_1} {n : Type u_4} {R : Type u_5} [inst : Sub n] [inst_1 : SMul R α] (k : R) (v : n → α),
Matrix.circulant (k • v) = k • Matrix.circulant v
The theorem `Matrix.circulant_smul` states that for any scalar `k` and any vector `v`, scaling the circulant matrix derived from `v` by `k` results in another circulant matrix that is derived from the scaled vector `k • v`. This holds for any types `α`, `n`, and `R`, where `α` is the type of elements in `v`, `n` is the index type of `v`, and `R` is the type of the scalar `k`, given that `n` has subtraction defined and `R` and `α` can be multiplied (i.e., `α` is a module over `R`).
More concisely: For any scalar `k` and vector `v` of type `α` with index type `n` where `n` supports subtraction and `α` is a module over scalar type `R`, the circulant matrix obtained from scaling `v` by `k` is equal to the circulant matrix of the scaled vector `k • v`.
|
Mathlib.LinearAlgebra.Matrix.Circulant._auxLemma.3
theorem Mathlib.LinearAlgebra.Matrix.Circulant._auxLemma.3 :
∀ {α : Sort u_1} [inst : Subsingleton α] (x y : α), (x = y) = True
This theorem, from the Mathlib's linear algebra library, asserts that for any type `α` that has a unique element (i.e., `α` is a subsingleton), and for any two elements `x` and `y` of that type, `x` is always equal to `y`. This is always True because in a subsingleton, there can only be one unique value. This is a fundamental property of types with a single inhabitant.
More concisely: In a subsingleton type, any two elements are equal.
|
Matrix.circulant_isSymm_apply
theorem Matrix.circulant_isSymm_apply :
∀ {α : Type u_1} {n : Type u_4} [inst : AddGroup n] {v : n → α},
(Matrix.circulant v).IsSymm → ∀ (i : n), v (-i) = v i
This theorem states that for any type `α`, any type `n` with an addition group structure, and any function `v` from `n` to `α`, if the circulant matrix generated by `v` is symmetric, then for all `i` in `n`, `v` of `-i` equals `v` of `i`. In other words, the function `v` is symmetric with respect to the origin in the addition group `n`.
More concisely: For any function `v` from an additive group `n` to a type `α`, if the circulant matrix of `v` is symmetric, then `v` is an even function, i.e., `v(-i) = v(i)` for all `i` in `n`.
|
Matrix.circulant_mul
theorem Matrix.circulant_mul :
∀ {α : Type u_1} {n : Type u_4} [inst : Semiring α] [inst_1 : Fintype n] [inst_2 : AddGroup n] (v w : n → α),
Matrix.circulant v * Matrix.circulant w = Matrix.circulant ((Matrix.circulant v).mulVec w)
This theorem states that for any semiring `α`, any type `n` that is a finite additive group, and any two vectors `v` and `w` of type `n → α`, the product of two circulant matrices generated by `v` and `w` is equal to the circulant matrix generated by the result of multiplying the circulant matrix of `v` with the vector `w`. In other words, if we denote the operation of creating a circulant matrix as `circulant` and matrix-vector multiplication as `mulVec`, the theorem says that `circulant v * circulant w = circulant ((circulant v).mulVec w)`.
More concisely: For any semiring `α` and finite additive group `n`, the product of two circulant matrices over `α` with vectors of type `n → α` as generators is equal to the circulant matrix generated by the element-wise product of their generators.
|
Matrix.circulant_isSymm_iff
theorem Matrix.circulant_isSymm_iff :
∀ {α : Type u_1} {n : Type u_4} [inst : AddGroup n] {v : n → α},
(Matrix.circulant v).IsSymm ↔ ∀ (i : n), v (-i) = v i
This theorem states that for any type `α`, any type `n` with an `AddGroup` instance, and any function `v : n → α`, the circulant matrix of `v` is symmetric if and only if `v` equals its reverse. In other words, the `(i, j)`th entry of the circulant matrix, which is `v(i - j)`, equals the `(j, i)`th entry, `v(j - i)`, for all `i` and `j`, if and only if `v(-i) = v(i)` for all `i`. This symmetry property of circulant matrices depends on the input vector `v` being equal to its reverse.
More concisely: For any function `v : ℕ → α` with type `α` and `ℕ` having an `AddGroup` instance, the circulant matrix of `v` is symmetric if and only if `v` is its own reverse.
|
Matrix.Fin.circulant_ite
theorem Matrix.Fin.circulant_ite :
∀ (α : Type u_6) [inst : Zero α] [inst_1 : One α] (n : ℕ),
(Matrix.circulant fun i => if ↑i = 0 then 1 else 0) = 1
The theorem `Matrix.Fin.circulant_ite` states that for any type `α` that has a zero and a one, and any natural number `n`, the circulant matrix generated by a function that maps `0` to `1` and all other numbers to `0` is equal to the identity matrix of type `α`. This result is crucial in the context of finite matrices where the index type is `Fin n`. Note that we use the condition `↑i = 0` rather than `i = 0` to account for the fact that `Fin 0` does not contain `0`. This approach differs from the one used in proving `Matrix.circulant_single`.
More concisely: For any type `α` with a zero and one, the circulant matrix of size `Fin n` generated by the function mapping `0` to `1` and all other numbers to `0` is equal to the identity matrix.
|
Matrix.circulant_mul_comm
theorem Matrix.circulant_mul_comm :
∀ {α : Type u_1} {n : Type u_4} [inst : CommSemigroup α] [inst_1 : AddCommMonoid α] [inst_2 : Fintype n]
[inst_3 : AddCommGroup n] (v w : n → α),
Matrix.circulant v * Matrix.circulant w = Matrix.circulant w * Matrix.circulant v
The theorem states that for any type `α` with an instance of a commutative semigroup and an additive commutative monoid, any type `n` with instances of a finite type and an additive commutative group, and any two functions `v` and `w` from `n` to `α`, the multiplication of the circulant matrix generated by `v` and the circulant matrix generated by `w` commutes. In other words, if you first generate a circulant matrix with `v` and multiply it by a circulant matrix generated by `w`, you'll get the same result as if you did the operations in reverse order: first generate a circulant matrix with `w` and then multiply it by a circulant matrix generated by `v`.
More concisely: For any commutative semigroup and additive commutative monoid instances on type `α`, and finite additive commutative groups instances on type `n`, the circulant matrices generated by functions `v` and `w` from `n` to `α` commute when multiplied.
|