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)}