Additivity of von Neumann entropy under the tensor (Kronecker) product

For density matrices ρ and σ over ℂ, the von Neumann entropy of their Kronecker product is the sum of the individual entropies:

S(ρ ⊗ σ) = S(ρ) + S(σ).

The proof passes to the multiset of eigenvalues of ρ ⊗ₖ σ, which by eigenvalues_kronecker_multiset is the multiset of pairwise products λᵢ · μⱼ. Writing negMulLog (λᵢ μⱼ) = μⱼ · negMulLog λᵢ + λᵢ · negMulLog μⱼ and using that each eigenvalue family sums to 1 (unit trace) collapses the double sum to S(ρ) + S(σ).

def Oseledets.OperatorEntropy.DensityMatrix.kron {nA : Type u_1} {nB : Type u_2} [Fintype nA] [DecidableEq nA] [Fintype nB] [DecidableEq nB] (ρ : DensityMatrix nA) (σ : DensityMatrix nB) : DensityMatrix (nA × nB)

The Kronecker (tensor) product of two density matrices, again a density matrix on the product index type nA × nB.

Equations

• ρ.kron σ = { val := Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ρ.val σ.val, posSemidef := ⋯, trace_one := ⋯ }

theorem Oseledets.OperatorEntropy.vonNeumannEntropy_additive_kronecker {nA : Type u_1} {nB : Type u_2} [Fintype nA] [DecidableEq nA] [Fintype nB] [DecidableEq nB] (ρ : DensityMatrix nA) (σ : DensityMatrix nB) : vonNeumannEntropy (ρ.kron σ) = vonNeumannEntropy ρ + vonNeumannEntropy σ

Additivity of von Neumann entropy under the tensor product. S(ρ ⊗ σ) = S(ρ) + S(σ).