Documentation

Oseledets.OperatorEntropy.Subadditivity

Subadditivity of the von Neumann entropy #

For a bipartite density matrix ρ on nA ⊗ nB with reduced density matrices ρ_A = Tr_B ρ and ρ_B = Tr_A ρ, the von Neumann entropy is subadditive: S(ρ) ≤ S(ρ_A) + S(ρ_B).

The proof is the elementary route through the scalar Klein / Peierls inequality (klein_scalar, Carlen, Trace Inequalities and Quantum Entropy, Thm 2.11; Nielsen–Chuang §11.3) — no Lieb concavity and no matrix logarithm / continuous functional calculus.

Writing M = G diag(p) Gᴴ, ρ_A = U diag(λ) Uᴴ, ρ_B = V diag(μ) Vᴴ from the spectral theorem and W = U ⊗ V, the doubly stochastic matrix D k m = |‖(Gᴴ W)ₖₘ‖² together with the product eigenvalue vector s (i,j) = λ i · μ j feeds Klein's inequality. The key linear-algebra input is the conjugation identity Tr_B(Wᴴ M W) = Uᴴ (Tr_B M) U (and its left analogue), which lets the marginals of D be read off as λ and μ.

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

The reduced density matrix on the left (A) factor: Tr_B ρ.

Equations
Instances For
    noncomputable def Oseledets.OperatorEntropy.DensityMatrix.partialTraceLeft {nA : Type u_1} {nB : Type u_2} [Fintype nA] [DecidableEq nA] [Fintype nB] [DecidableEq nB] (ρ : DensityMatrix (nA × nB)) :

    The reduced density matrix on the right (B) factor: Tr_A ρ.

    Equations
    Instances For

      Subadditivity of the von Neumann entropy. S(ρ) ≤ S(Tr_B ρ) + S(Tr_A ρ) for a bipartite density matrix ρ.