Kronecker quadratic forms on vectorized matrices

The quadratic form of a Kronecker product V ⊗ₖ U on column-stacked matrices is a trace. For positive semidefinite U and V, this makes trace (Tᵀ * U * T * V) nonnegative.

Main results

• Matrix.vec_dotProduct_kronecker_mulVec_vec: the trace formula for the bilinear form of V ⊗ₖ U on vectorized matrices.
• Matrix.IsSymm.vec_dotProduct_kronecker_mulVec_vec: the same formula for symmetric V, without the transpose.
• Matrix.PosSemidef.trace_transpose_mul_mul_mul_nonneg: nonnegativity of trace (Tᵀ * U * T * V) for positive semidefinite U and V.

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

The quadratic form of a Kronecker product on column-stacked matrices is a trace: vec A ⬝ᵥ (V ⊗ₖ U) *ᵥ vec B = trace (Aᵀ * U * B * Vᵀ).

theorem Matrix.IsSymm.vec_dotProduct_kronecker_mulVec_vec {R : Type u_1} {l : Type u_2} {m : Type u_3} {n : Type u_4} [Fintype l] [Fintype m] [Fintype n] [NonUnitalCommSemiring R] {V : Matrix n n R} (hV : V.IsSymm) (A : Matrix l n R) (U : Matrix l m R) (B : Matrix m n R) : A.vec ⬝ᵥ (kroneckerMap (fun (x1 x2 : R) => x1 * x2) V U).mulVec B.vec = (A.transpose * U * B * V).trace

For symmetric V, the Kronecker quadratic form on column-stacked matrices is vec A ⬝ᵥ (V ⊗ₖ U) *ᵥ vec B = trace (Aᵀ * U * B * V).

theorem Matrix.PosSemidef.trace_transpose_mul_mul_mul_nonneg {m : Type u_3} {n : Type u_4} [Fintype m] [Fintype n] {U : Matrix m m ℝ} {V : Matrix n n ℝ} (hU : U.PosSemidef) (hV : V.PosSemidef) (T : Matrix m n ℝ) : 0 ≤ (T.transpose * U * T * V).trace

For positive semidefinite U and V, the covariance quadratic form trace (Tᵀ * U * T * V) is nonnegative. It is the quadratic form of V ⊗ₖ U at vec T.