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

References