Documentation

Mathlib.Data.Matrix.Vec

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 #

source
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
Instances For
    source
    @[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)
    source
    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
    source
    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
    source
    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
    source
    theorem Matrix.vec_bijective {m : Type u_3} {n : Type u_2} {R : Type u_1} :
    Function.Bijective vec
    source
    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
    source
    @[simp]
    theorem Matrix.vec_zero {m : Type u_3} {n : Type u_2} {R : Type u_1} [Zero R] :
    vec 0 = 0
    source
    @[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
    source
    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
    source
    @[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
    source
    @[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
    source
    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
    source
    theorem Matrix.vec_dotProduct_vec {m : Type u_2} {n : Type u_3} {R : Type u_1} [NonUnitalNonAssocSemiring R] [Fintype m] [Fintype n] (A B : Matrix m n R) :
    A.vec ⬝ᵥ B.vec = (A.transpose * B).trace
    source
    theorem Matrix.star_vec_dotProduct_vec {m : Type u_2} {n : Type u_3} {R : Type u_1} [NonUnitalNonAssocSemiring R] [StarRing R] [Fintype m] [Fintype n] (A B : Matrix m n R) :
    star A.vec ⬝ᵥ B.vec = (A.conjTranspose * B).trace
    source
    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
    source
    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.

    source
    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.

    source
    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
    source
    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
    source
    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
    source
    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)