Entanglement of formation of quantum state

“The asymptotic number of Bell pairs required to prepare with LOCC a system in the bipartite state ρ.”

import Quantum_state
import Quantum_entropy

def entanglement_of_formation [quantum_state ρ] : ℝ :=
inf {∑ i, (p i) * quantum_entropy Tr₂ (ρ i) | rnd_var(p) ∧ ∑i,(p i)*(ρ i)=ρ ∧ ∀i,quantum_state(ρ i)∧pure(ρ i)} 

References