Research proof index

Entanglement of Formation of bipartite systems. It is the convex roof extension of the von Neumann entropy of one of the subsystems (here chosen to be the left one, but see Entropy.Sᵥₙ_of_partial_eq). The function Sᵥₙ ∘ traceRight ∘ pure is phase-invariant because pure maps phase-equivalent kets to the same mixed state, so it descends to `KetUpToPha...

Triangle inequality for pure tripartite states: S(A) ≤ S(B) + S(C).

Strong subadditivity on a tripartite system

"Ordinary" subadditivity of von Neumann entropy

Weak monotonicity, version with partial traces.

Step 1 (Variational formula): For α > 1, the trace functional equals the supremum of f_α over all PSD H: Q̃_α(ρ‖σ) = ⨆ (H : HermitianMat d ℂ) (_ : 0 ≤ H), f_alpha α H ρ σ. The optimizer is H_hat = σ^γ (σ^γ ρ σ^γ)^{α−1} σ^γ.