Rains relative entropy
“Rains relative entropy of bipartite Quantum state
upper bounds Distillable entanglement of quantum state.”
“efficiently computable by convex programming.”
import Quantum_relative_entropy import Trace_distance variables (ℋ₁ ℋ₂ : Type) [complex_Hilbert_space ℋ₁] [complex_Hilbert_space ℋ₂] (ρ σ : ℋ₁⊗ℋ₂ →ₗ[ℂ] ℋ₁⊗ℋ₂) [quantum_state ρ] [pos_semidef σ] [supp ρ ⊆ supp σ] def PPT (σ) := σ ≥ 0 ∧ ∥pTr₂ σ∥₁ ≤ 1 def Rains_relative_entropy (ρ) := min {D(ρ∥σ) | PPT σ}