The Kronecker product of a family of matrices

The k-fold tensor product M₁ ⊗ ⋯ ⊗ M_k of matrices on ℂ^ι, as a matrix on ℂ^{Fin k → ι}: (⊗ᵢ Mᵢ) v w = ∏ᵢ Mᵢ (v i) (w i). This is what the k-fold tensor power of a strategy measures with (MIPRE.SyncStrategy.tensorPow, Background/Repetition/TensorPower.lean), and the four facts about it that the value and PCC computations use: it is multiplicative (tensorFamily_mul), compatible with the adjoint (tensorFamily_conjTranspose), sends the constant family 1 to 1 (tensorFamily_one), sums coordinatewise (sum_tensorFamily) and has trace the product of the traces (trace_tensorFamily). All are Fintype.prod_sum, the distributivity of a product of sums over Fin k into a sum over Fin k → ι.

Mathlib's Matrix.kronecker is the binary case with the product index ι × ι; the family form is more convenient than iterating it, because Fin k → ι needs no reassociation.

def MIPRE.tensorFamily {k : ℕ} {ι : Type u_1} (M : Fin k → Matrix ι ι ℂ) : Matrix (Fin k → ι) (Fin k → ι) ℂ

The tensor product ⊗ᵢ Mᵢ of a family of matrices, as a matrix indexed by Fin k → ι.

Equations

• MIPRE.tensorFamily M = Matrix.of fun (v w : Fin k → ι) => ∏ i : Fin k, M i (v i) (w i)

@[simp]

theorem MIPRE.tensorFamily_apply {k : ℕ} {ι : Type u_1} (M : Fin k → Matrix ι ι ℂ) (v w : Fin k → ι) : tensorFamily M v w = ∏ i : Fin k, M i (v i) (w i)

theorem MIPRE.tensorFamily_mul {k : ℕ} {ι : Type u_1} [Fintype ι] (M N : Fin k → Matrix ι ι ℂ) : tensorFamily M * tensorFamily N = tensorFamily fun (i : Fin k) => M i * N i

theorem MIPRE.tensorFamily_conjTranspose {k : ℕ} {ι : Type u_1} (M : Fin k → Matrix ι ι ℂ) : (tensorFamily M).conjTranspose = tensorFamily fun (i : Fin k) => (M i).conjTranspose

theorem MIPRE.tensorFamily_one {k : ℕ} {ι : Type u_1} [DecidableEq ι] : (tensorFamily fun (x : Fin k) => 1) = 1

theorem MIPRE.trace_tensorFamily {k : ℕ} {ι : Type u_1} [Fintype ι] (M : Fin k → Matrix ι ι ℂ) : (tensorFamily M).trace = ∏ i : Fin k, (M i).trace

theorem MIPRE.sum_tensorFamily {k : ℕ} {ι : Type u_1} {A : Type u_2} [Fintype A] (M : Fin k → A → Matrix ι ι ℂ) : (∑ a : Fin k → A, tensorFamily fun (i : Fin k) => M i (a i)) = tensorFamily fun (i : Fin k) => ∑ a : A, M i a

theorem MIPRE.tensorFamily_mul_self {k : ℕ} {ι : Type u_1} [Fintype ι] {M : Fin k → Matrix ι ι ℂ} (h : ∀ (i : Fin k), M i * M i = M i) : tensorFamily M * tensorFamily M = tensorFamily M

The tensor product of a family of idempotents is idempotent.

theorem MIPRE.tensorFamily_star {k : ℕ} {ι : Type u_1} {M : Fin k → Matrix ι ι ℂ} (h : ∀ (i : Fin k), star (M i) = M i) : star (tensorFamily M) = tensorFamily M

The tensor product of a family of self-adjoint matrices is self-adjoint.