Block-diagonal finite matrix operators

This module contains block-diagonal trace and positive-semidefinite order facts for finite complex matrices. The canonical SDP block algebra in Section 9 uses these lemmas to compare the paper's block form with Mathlib's Matrix.blockDiagonal.

theorem Matrix.blockDiagonal_eq_sum_kronecker_diagonal {o : Type u_1} {m : Type u_2} [Fintype o] [DecidableEq o] [Finite m] (B : o → Matrix m m ℂ) : blockDiagonal B = ∑ b : o, (B b).kronecker (diagonal fun (c : o) => if c = b then 1 else 0)

A block-diagonal matrix is the sum of its blocks tensored with the coordinate projections on the block index.

def Matrix.blockDiagonalLinearMap (R : Type u_1) (m : Type u_2) (n : Type u_3) (o : Type u_4) (α : Type u_5) [Semiring R] [DecidableEq o] [AddCommMonoid α] [Module R α] : (o → Matrix m n α) →ₗ[R] Matrix (m × o) (n × o) α

Matrix.blockDiagonal as a linear map.

Mathlib provides Matrix.blockDiagonalAddMonoidHom and Matrix.blockDiagonal_smul; this declaration packages these two facts in the linear form needed by finite-dimensional block SDP arguments.

Equations

• Matrix.blockDiagonalLinearMap R m n o α = { toFun := Matrix.blockDiagonal, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Matrix.blockDiagonalLinearMap_apply (R : Type u_1) (m : Type u_2) (n : Type u_3) (o : Type u_4) (α : Type u_5) [Semiring R] [DecidableEq o] [AddCommMonoid α] [Module R α] (B : o → Matrix m n α) : (blockDiagonalLinearMap R m n o α) B = blockDiagonal B

theorem Matrix.blockDiagonal_nonneg {o : Type u_1} {m : Type u_2} [Finite o] [DecidableEq o] [Finite m] (B : o → Matrix m m ℂ) (hB : ∀ (b : o), 0 ≤ B b) : 0 ≤ blockDiagonal B

A block-diagonal complex matrix is positive semidefinite when all of its diagonal blocks are positive semidefinite.

theorem Matrix.blockDiagonal_nonneg_iff {o : Type u_1} {m : Type u_2} [Finite o] [DecidableEq o] [Finite m] (B : o → Matrix m m ℂ) : 0 ≤ blockDiagonal B ↔ ∀ (b : o), 0 ≤ B b

A block-diagonal complex matrix is positive semidefinite exactly when each of its diagonal blocks is positive semidefinite.