Vectorization of matrices

This file defines Matrix.vec A, the vectorization of a matrix A, formed by stacking the columns of A into a single large column vector.

Since mathlib indices matrices by arbitrary types rather than Fin n, the result of Matrix.vec on A : Matrix m n R is indexed by n × m. The Fin (n * m) interpretation can be restored by composing with finProdFinEquiv.symm:

-- ![1, 2, 3, 4]
#eval vec !![1, 3; 2, 4] ∘ finProdFinEquiv.symm

While it may seem more natural to index by m × n, keeping the indices in the same order, this would amount to stacking the rows into one long row, and goes against the literature. If you want this function, you can write Matrix.vec Aᵀ instead.

References

• Wikipedia

def Matrix.vec {m : Type u_1} {n : Type u_2} {R : Type u_3} (A : Matrix m n R) : n × m → R

All the matrix entries, arranged into one column.

Equations

• A.vec ij = A ij.2 ij.1

@[simp]

theorem Matrix.vec_of {m : Type u_2} {n : Type u_1} {R : Type u_3} (f : m → n → R) : (of f).vec = Function.uncurry (flip f)

theorem Matrix.vec_transpose {m : Type u_1} {n : Type u_2} {R : Type u_3} (A : Matrix m n R) : A.transpose.vec = A.vec ∘ Prod.swap

theorem Matrix.vec_eq_uncurry {m : Type u_1} {n : Type u_2} {R : Type u_3} (A : Matrix m n R) : A.vec = Function.uncurry fun (i : n) (j : m) => A j i

theorem Matrix.vec_inj {m : Type u_1} {n : Type u_2} {R : Type u_3} {A B : Matrix m n R} : A.vec = B.vec ↔ A = B

theorem Matrix.vec_bijective {m : Type u_3} {n : Type u_2} {R : Type u_1} : Function.Bijective vec

theorem Matrix.vec_map {m : Type u_1} {n : Type u_2} {R : Type u_3} {S : Type u_4} (A : Matrix m n R) (f : R → S) : (A.map f).vec = f ∘ A.vec

@[simp]

theorem Matrix.vec_zero {m : Type u_3} {n : Type u_2} {R : Type u_1} [Zero R] : vec 0 = 0

@[simp]

theorem Matrix.vec_eq_zero_iff {m : Type u_2} {n : Type u_3} {R : Type u_1} [Zero R] {A : Matrix m n R} : A.vec = 0 ↔ A = 0

@[simp]

theorem Matrix.vec_add {m : Type u_2} {n : Type u_3} {R : Type u_1} [Add R] (A B : Matrix m n R) : (A + B).vec = A.vec + B.vec

theorem Matrix.vec_neg {m : Type u_2} {n : Type u_3} {R : Type u_1} [Neg R] (A : Matrix m n R) : (-A).vec = -A.vec

@[simp]

theorem Matrix.vec_sub {m : Type u_2} {n : Type u_3} {R : Type u_1} [Sub R] (A B : Matrix m n R) : (A - B).vec = A.vec - B.vec

@[simp]

theorem Matrix.vec_smul {m : Type u_3} {n : Type u_4} {R : Type u_2} {α : Type u_1} [SMul α R] (r : α) (A : Matrix m n R) : (r • A).vec = r • A.vec

theorem Matrix.vec_sum {ι : Type u_2} {m : Type u_3} {n : Type u_4} {R : Type u_1} [AddCommMonoid R] (s : Finset ι) (A : ι → Matrix m n R) : (∑ i ∈ s, A i).vec = ∑ i ∈ s, (A i).vec

theorem Matrix.vec_dotProduct_vec {m : Type u_2} {n : Type u_3} {R : Type u_1} [AddCommMonoid R] [Mul R] [Fintype m] [Fintype n] (A B : Matrix m n R) : A.vec ⬝ᵥ B.vec = (A.transpose * B).trace

theorem Matrix.star_vec {m : Type u_2} {n : Type u_3} {R : Type u_1} [Star R] (x : Matrix m n R) : star x.vec = (x.map star).vec

theorem Matrix.star_vec_dotProduct_vec {m : Type u_2} {n : Type u_3} {R : Type u_1} [AddCommMonoid R] [Mul R] [Star R] [Fintype m] [Fintype n] (A B : Matrix m n R) : star A.vec ⬝ᵥ B.vec = (A.conjTranspose * B).trace

theorem Matrix.vec_hadamard {m : Type u_2} {n : Type u_3} {R : Type u_1} [Mul R] (A B : Matrix m n R) : (A.hadamard B).vec = A.vec * B.vec

@[simp]

theorem Matrix.vec_single {m : Type u_1} {n : Type u_2} {R : Type u_3} [DecidableEq m] [DecidableEq n] [Zero R] (i : m) (j : n) (r : R) : (single i j r).vec = Pi.single (j, i) r

theorem Matrix.hadamard_kronecker_hadamard {l : Type u_1} {m : Type u_2} {n : Type u_4} {p : Type u_5} {R : Type u_3} [CommSemigroup R] (A B : Matrix l m R) (C D : Matrix n p R) : kroneckerMap (fun (x1 x2 : R) => x1 * x2) (A.hadamard B) (C.hadamard D) = (kroneckerMap (fun (x1 x2 : R) => x1 * x2) A C).hadamard (kroneckerMap (fun (x1 x2 : R) => x1 * x2) B D)

theorem Matrix.kronecker_hadamard_kronecker {l : Type u_1} {m : Type u_2} {n : Type u_4} {p : Type u_5} {R : Type u_3} [CommSemigroup R] (A : Matrix l m R) (B : Matrix n p R) (C : Matrix l m R) (D : Matrix n p R) : (kroneckerMap (fun (x1 x2 : R) => x1 * x2) A B).hadamard (kroneckerMap (fun (x1 x2 : R) => x1 * x2) C D) = kroneckerMap (fun (x1 x2 : R) => x1 * x2) (A.hadamard C) (B.hadamard D)

theorem Matrix.kronecker_mulVec_vec_of_commute {l : Type u_1} {m : Type u_2} {n : Type u_4} {p : Type u_5} {R : Type u_3} [NonUnitalSemiring R] [Fintype m] [Fintype n] (A : Matrix l m R) (X : Matrix m n R) (B : Matrix p n R) (hB : ∀ (x : R) (i : p) (j : n), Commute x (B i j)) : (kroneckerMap (fun (x1 x2 : R) => x1 * x2) B A).mulVec X.vec = (A * X * B.transpose).vec

Technical lemma shared with kronecker_mulVec_vec and vec_mul_eq_mulVec.

theorem Matrix.vec_vecMul_kronecker_of_commute {l : Type u_2} {m : Type u_1} {n : Type u_4} {p : Type u_5} {R : Type u_3} [NonUnitalSemiring R] [Fintype m] [Fintype n] (A : Matrix m l R) (X : Matrix m n R) (B : Matrix n p R) (hA : ∀ (x : R) (i : m) (j : l), Commute (A i j) x) : vecMul X.vec (kroneckerMap (fun (x1 x2 : R) => x1 * x2) B A) = (A.transpose * X * B).vec

Technical lemma shared with vec_vecMul_kronecker and vec_mul_eq_vecMul.

theorem Matrix.kronecker_mulVec_vec {l : Type u_1} {m : Type u_2} {n : Type u_4} {p : Type u_5} {R : Type u_3} [NonUnitalCommSemiring R] [Fintype m] [Fintype n] (A : Matrix l m R) (X : Matrix m n R) (B : Matrix p n R) : (kroneckerMap (fun (x1 x2 : R) => x1 * x2) B A).mulVec X.vec = (A * X * B.transpose).vec

theorem Matrix.vec_vecMul_kronecker {l : Type u_2} {m : Type u_1} {n : Type u_4} {p : Type u_5} {R : Type u_3} [NonUnitalCommSemiring R] [Fintype m] [Fintype n] (A : Matrix m l R) (X : Matrix m n R) (B : Matrix n p R) : vecMul X.vec (kroneckerMap (fun (x1 x2 : R) => x1 * x2) B A) = (A.transpose * X * B).vec

theorem Matrix.vec_mul_eq_mulVec {l : Type u_2} {m : Type u_3} {n : Type u_1} {R : Type u_4} [Semiring R] [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix l m R) (B : Matrix m n R) : (A * B).vec = (kroneckerMap (fun (x1 x2 : R) => x1 * x2) 1 A).mulVec B.vec

theorem Matrix.vec_mul_eq_vecMul {m : Type u_1} {n : Type u_2} {p : Type u_4} {R : Type u_3} [Semiring R] [Fintype m] [Fintype n] [DecidableEq m] (A : Matrix m n R) (B : Matrix n p R) : (A * B).vec = vecMul A.vec (kroneckerMap (fun (x1 x2 : R) => x1 * x2) B 1)

theorem Matrix.dotProduct_hadamard_mulVec_eq_kronecker {m : Type u_1} {n : Type u_2} {R : Type u_3} [NonUnitalSemiring R] [DecidableEq m] [Fintype m] [DecidableEq n] [Fintype n] (x : m → R) (A B : Matrix m n R) (x' : n → R) : x ⬝ᵥ (A.hadamard B).mulVec x' = (diagonal x).vec ⬝ᵥ (kroneckerMap (fun (x1 x2 : R) => x1 * x2) A B).mulVec (diagonal x').vec

The Hadamard bilinear form equals the Kronecker bilinear form on diagonal embeddings.

theorem Matrix.star_dotProduct_hadamard_mulVec_eq_kronecker {m : Type u_2} {n : Type u_3} {R : Type u_1} [NonUnitalSemiring R] [DecidableEq m] [Fintype m] [DecidableEq n] [Fintype n] [StarAddMonoid R] (x : m → R) (A B : Matrix m n R) (x' : n → R) : star x ⬝ᵥ (A.hadamard B).mulVec x' = star (diagonal x).vec ⬝ᵥ (kroneckerMap (fun (x1 x2 : R) => x1 * x2) A B).mulVec (diagonal x').vec

The starred Hadamard bilinear form equals the starred Kronecker bilinear form on diagonal embeddings.