The functional calculus of Kronecker products

For square matrices A over 𝕜 = ℝ or ℂ (any RCLike field), the maps A ↦ A ⊗ₖ 1 and B ↦ 1 ⊗ₖ B are continuous unital ⋆-algebra homomorphisms, so they commute with the continuous functional calculus: cfc f (A ⊗ₖ 1) = cfc f A ⊗ₖ 1 and cfc f (1 ⊗ₖ B) = 1 ⊗ₖ cfc f B. The two factors A ⊗ₖ 1 and 1 ⊗ₖ B of A ⊗ₖ B commute, so for positive definite A and B the logarithm of their Kronecker product splits as a sum, log (A ⊗ₖ B) = log A ⊗ₖ 1 + 1 ⊗ₖ log B.

When the index m × n labels a basis of the tensor product of two finite quantum systems, this is the additivity of the logarithm of a product state, which underlies the subadditivity of the von Neumann entropy (TauCeti/Analysis/Matrix/Entropy.lean).

Main results

• Matrix.cfc_kronecker_one, Matrix.cfc_one_kronecker: the functional calculus commutes with tensoring by the identity on either side;
• Matrix.PosDef.cfc_log_kronecker: log (A ⊗ₖ B) = log A ⊗ₖ 1 + 1 ⊗ₖ log B for positive definite A and B.

@[simp]

theorem Matrix.cfc_kronecker_one {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike 𝕜] [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (f : ℝ → ℝ) (A : Matrix m m 𝕜) : cfc f (kroneckerMap (fun (x1 x2 : 𝕜) => x1 * x2) A 1) = kroneckerMap (fun (x1 x2 : 𝕜) => x1 * x2) (cfc f A) 1

The functional calculus commutes with tensoring by the identity on the right.

@[simp]

theorem Matrix.cfc_one_kronecker {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike 𝕜] [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (f : ℝ → ℝ) (B : Matrix n n 𝕜) : cfc f (kroneckerMap (fun (x1 x2 : 𝕜) => x1 * x2) 1 B) = kroneckerMap (fun (x1 x2 : 𝕜) => x1 * x2) 1 (cfc f B)

The functional calculus commutes with tensoring by the identity on the left.

theorem Matrix.PosDef.cfc_log_kronecker {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike 𝕜] [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] {A : Matrix m m 𝕜} {B : Matrix n n 𝕜} (hA : A.PosDef) (hB : B.PosDef) : cfc Real.log (kroneckerMap (fun (x1 x2 : 𝕜) => x1 * x2) A B) = kroneckerMap (fun (x1 x2 : 𝕜) => x1 * x2) (cfc Real.log A) 1 + kroneckerMap (fun (x1 x2 : 𝕜) => x1 * x2) 1 (cfc Real.log B)

The logarithm of the Kronecker product of two positive definite matrices is log A ⊗ₖ 1 + 1 ⊗ₖ log B.