Kronecker products of symmetric and positive definite matrices

The block-diagonal product 1 ⊗ₖ A preserves positive definiteness over any star ring with an additive order. Both index types may be infinite, since positive definiteness tests only finitely supported vectors. This covers orthogonal sums of copies of one rational Gram matrix. The symmetry result needs only multiplication, and the finite identity for the quadratic expression holds over a nonassociative semiring with an arbitrary star operation.

Main results

• Matrix.IsSymm.kronecker: the Kronecker product of symmetric matrices is symmetric.
• Matrix.finsupp_sum_one_kronecker: the finitely supported quadratic expression for 1 ⊗ₖ A decomposes into the expressions for A on its blocks.
• Matrix.PosDef.one_kronecker: if A is positive definite, so is 1 ⊗ₖ A.

theorem Matrix.IsSymm.kronecker {R : Type u_1} {m : Type u_2} {n : Type u_3} [Mul R] {A : Matrix m m R} {B : Matrix n n R} (hA : A.IsSymm) (hB : B.IsSymm) : (kroneckerMap (fun (x1 x2 : R) => x1 * x2) A B).IsSymm

The Kronecker product of symmetric matrices is symmetric.

theorem Matrix.star_dotProduct_one_kronecker_mulVec {R : Type u_1} {m : Type u_2} {n : Type u_3} [NonAssocSemiring R] [Star R] [Fintype m] [DecidableEq m] [Fintype n] (A : Matrix n n R) (x : m × n → R) : star x ⬝ᵥ (kroneckerMap (fun (x1 x2 : R) => x1 * x2) 1 A).mulVec x = ∑ i : m, (star fun (j : n) => x (i, j)) ⬝ᵥ A.mulVec fun (j : n) => x (i, j)

The quadratic expression for 1 ⊗ₖ A is the sum of those for A on the blocks.

theorem Matrix.finsupp_sum_one_kronecker {R : Type u_1} {m : Type u_2} {n : Type u_3} [NonAssocSemiring R] [Star R] [DecidableEq m] (A : Matrix n n R) (x : m × n →₀ R) : (x.sum fun (i : m × n) (xi : R) => x.sum fun (j : m × n) (xj : R) => star xi * kroneckerMap (fun (x1 x2 : R) => x1 * x2) 1 A i j * xj) = x.curry.sum fun (x : m) (y : n →₀ R) => y.sum fun (i : n) (yi : R) => y.sum fun (j : n) (yj : R) => star yi * A i j * yj

The finitely supported quadratic expression for 1 ⊗ₖ A is the sum of those for A on the blocks.

theorem Matrix.PosDef.one_kronecker {R : Type u_1} {m : Type u_2} {n : Type u_3} [Ring R] [PartialOrder R] [StarRing R] [IsOrderedAddMonoid R] [DecidableEq m] {A : Matrix n n R} (hA : A.PosDef) : (kroneckerMap (fun (x1 x2 : R) => x1 * x2) 1 A).PosDef

If A is positive definite, then so is the block-diagonal matrix 1 ⊗ₖ A.