Logarithmic negativity

import Quantum_channel
import Partial_transpose
import Separable

/-- Entanglement measure. -/
def log_negativity [quantum_state ρ] : ℝ := 
log₂ ∥partial_transpose ρ∥₁

theorem zero_log_negativity_of_separable_state :
separable ρ → log_negativity ρ = 0 := sorry

References

• Lami2022;